Theorem atcvatlem 10220

Description: Lemma for atcvat 10221.

Hypothesis

Ref	Expression
atoml.1	|- A e. CH

Assertion

Ref	Expression
atcvatlem	|- (((B e. Atoms /\ C e. Atoms) /\ (A =/= 0H /\ A (. (B vH C))) -> (-. B (_ A -> A e. Atoms))

Proof of Theorem atcvatlem

Step	Hyp	Ref	Expression
1		atnem0 10212	. . . . . . . . . . . . . . . 16 |- ((x e. Atoms /\ B e. Atoms) -> (-. x = B <-> (x i^i B) = 0H))
2		sseq1 2072	. . . . . . . . . . . . . . . . . . . 20 |- (x = B -> (x (_ A <-> B (_ A))
3	2	biimpcd 155	. . . . . . . . . . . . . . . . . . 19 |- (x (_ A -> (x = B -> B (_ A))
4	3	con3d 95	. . . . . . . . . . . . . . . . . 18 |- (x (_ A -> (-. B (_ A -> -. x = B))
5	4	imp 350	. . . . . . . . . . . . . . . . 17 |- ((x (_ A /\ -. B (_ A) -> -. x = B)
6	5	adantrl 394	. . . . . . . . . . . . . . . 16 |- ((x (_ A /\ (A (. (B vH C) /\ -. B (_ A)) -> -. x = B)
7	1, 6	syl5bi 208	. . . . . . . . . . . . . . 15 |- ((x e. Atoms /\ B e. Atoms) -> ((x (_ A /\ (A (. (B vH C) /\ -. B (_ A)) -> (x i^i B) = 0H))
8		cvp 10210	. . . . . . . . . . . . . . . . 17 |- ((x e. CH /\ B e. Atoms) -> ((x i^i B) = 0H <-> x <o (x vH B)))
9		chjcomt 9344	. . . . . . . . . . . . . . . . . . 19 |- ((x e. CH /\ B e. CH) -> (x vH B) = (B vH x))
10		atelch 10179	. . . . . . . . . . . . . . . . . . 19 |- (B e. Atoms -> B e. CH)
11	9, 10	sylan2 451	. . . . . . . . . . . . . . . . . 18 |- ((x e. CH /\ B e. Atoms) -> (x vH B) = (B vH x))
12	11	breq2d 2620	. . . . . . . . . . . . . . . . 17 |- ((x e. CH /\ B e. Atoms) -> (x <o (x vH B) <-> x <o (B vH x)))
13	8, 12	bitrd 526	. . . . . . . . . . . . . . . 16 |- ((x e. CH /\ B e. Atoms) -> ((x i^i B) = 0H <-> x <o (B vH x)))
14		atelch 10179	. . . . . . . . . . . . . . . 16 |- (x e. Atoms -> x e. CH)
15	13, 14	sylan 448	. . . . . . . . . . . . . . 15 |- ((x e. Atoms /\ B e. Atoms) -> ((x i^i B) = 0H <-> x <o (B vH x)))
16	7, 15	sylibd 202	. . . . . . . . . . . . . 14 |- ((x e. Atoms /\ B e. Atoms) -> ((x (_ A /\ (A (. (B vH C) /\ -. B (_ A)) -> x <o (B vH x)))
17	16	ancoms 436	. . . . . . . . . . . . 13 |- ((B e. Atoms /\ x e. Atoms) -> ((x (_ A /\ (A (. (B vH C) /\ -. B (_ A)) -> x <o (B vH x)))
18	17	adantlr 393	. . . . . . . . . . . 12 |- (((B e. Atoms /\ C e. Atoms) /\ x e. Atoms) -> ((x (_ A /\ (A (. (B vH C) /\ -. B (_ A)) -> x <o (B vH x)))
19	18	imp 350	. . . . . . . . . . 11 |- ((((B e. Atoms /\ C e. Atoms) /\ x e. Atoms) /\ (x (_ A /\ (A (. (B vH C) /\ -. B (_ A))) -> x <o (B vH x))
20		chub1t 9345	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((B e. CH /\ x e. CH) -> B (_ (B vH x))
21	20, 10, 14	syl2an 454	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((B e. Atoms /\ x e. Atoms) -> B (_ (B vH x))
22	21	3adant3 797	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((B e. Atoms /\ x e. Atoms /\ C e. Atoms) -> B (_ (B vH x))
23	22	adantr 389	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((B e. Atoms /\ x e. Atoms /\ C e. Atoms) /\ ((x (_ A /\ -. B (_ A) /\ A (. (B vH C))) -> B (_ (B vH x))
24		sstr 2062	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x (_ A /\ A (_ (B vH C)) -> x (_ (B vH C))
25		pssss 2133	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (A (. (B vH C) -> A (_ (B vH C))
26	24, 25	sylan2 451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((x (_ A /\ A (. (B vH C)) -> x (_ (B vH C))
27	26	adantlr 393	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((x (_ A /\ -. B (_ A) /\ A (. (B vH C)) -> x (_ (B vH C))
28	27	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((B e. Atoms /\ x e. Atoms /\ C e. Atoms) /\ ((x (_ A /\ -. B (_ A) /\ A (. (B vH C))) -> x (_ (B vH C))
29	1, 5	syl5bi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((x e. Atoms /\ B e. Atoms) -> ((x (_ A /\ -. B (_ A) -> (x i^i B) = 0H))
30	29	ancoms 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((B e. Atoms /\ x e. Atoms) -> ((x (_ A /\ -. B (_ A) -> (x i^i B) = 0H))
31	30	3adant3 797	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((B e. Atoms /\ x e. Atoms /\ C e. Atoms) -> ((x (_ A /\ -. B (_ A) -> (x i^i B) = 0H))
32	31	imp 350	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((B e. Atoms /\ x e. Atoms /\ C e. Atoms) /\ (x (_ A /\ -. B (_ A)) -> (x i^i B) = 0H)
33		incom 2198	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (B i^i x) = (x i^i B)
34	32, 33	syl5eq 1511	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((B e. Atoms /\ x e. Atoms /\ C e. Atoms) /\ (x (_ A /\ -. B (_ A)) -> (B i^i x) = 0H)
35	34	adantrr 395	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((B e. Atoms /\ x e. Atoms /\ C e. Atoms) /\ ((x (_ A /\ -. B (_ A) /\ A (. (B vH C))) -> (B i^i x) = 0H)
36		atexcht 10216	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((B e. CH /\ x e. Atoms /\ C e. Atoms) -> ((x (_ (B vH C) /\ (B i^i x) = 0H) -> C (_ (B vH x)))
37	36, 10	syl3an1 857	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((B e. Atoms /\ x e. Atoms /\ C e. Atoms) -> ((x (_ (B vH C) /\ (B i^i x) = 0H) -> C (_ (B vH x)))
38	37	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((B e. Atoms /\ x e. Atoms /\ C e. Atoms) /\ ((x (_ A /\ -. B (_ A) /\ A (. (B vH C))) -> ((x (_ (B vH C) /\ (B i^i x) = 0H) -> C (_ (B vH x)))
39	28, 35, 38	mp2and 701	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((B e. Atoms /\ x e. Atoms /\ C e. Atoms) /\ ((x (_ A /\ -. B (_ A) /\ A (. (B vH C))) -> C (_ (B vH x))
40	23, 39	jca 288	. . . . . . . . . . . . . . . . . . . . . 22 |- (((B e. Atoms /\ x e. Atoms /\ C e. Atoms) /\ ((x (_ A /\ -. B (_ A) /\ A (. (B vH C))) -> (B (_ (B vH x) /\ C (_ (B vH x)))
41		3simp1 786	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((B e. CH /\ x e. CH /\ C e. CH) -> B e. CH)
42		3simp3 788	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((B e. CH /\ x e. CH /\ C e. CH) -> C e. CH)
43		chjclt 9244	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((B e. CH /\ x e. CH) -> (B vH x) e. CH)
44	43	3adant3 797	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((B e. CH /\ x e. CH /\ C e. CH) -> (B vH x) e. CH)
45	41, 42, 44	3jca 817	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((B e. CH /\ x e. CH /\ C e. CH) -> (B e. CH /\ C e. CH /\ (B vH x) e. CH))
46		atelch 10179	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (C e. Atoms -> C e. CH)
47	45, 10, 14, 46	syl3an 866	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((B e. Atoms /\ x e. Atoms /\ C e. Atoms) -> (B e. CH /\ C e. CH /\ (B vH x) e. CH))
48		chlubt 9347	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((B e. CH /\ C e. CH /\ (B vH x) e. CH) -> ((B (_ (B vH x) /\ C (_ (B vH x)) <-> (B vH C) (_ (B vH x)))
49	47, 48	syl 10	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((B e. Atoms /\ x e. Atoms /\ C e. Atoms) -> ((B (_ (B vH x) /\ C (_ (B vH x)) <-> (B vH C) (_ (B vH x)))
50	49	adantr 389	. . . . . . . . . . . . . . . . . . . . . 22 |- (((B e. Atoms /\ x e. Atoms /\ C e. Atoms) /\ ((x (_ A /\ -. B (_ A) /\ A (. (B vH C))) -> ((B (_ (B vH x) /\ C (_ (B vH x)) <-> (B vH C) (_ (B vH x)))
51	40, 50	mpbid 195	. . . . . . . . . . . . . . . . . . . . 21 |- (((B e. Atoms /\ x e. Atoms /\ C e. Atoms) /\ ((x (_ A /\ -. B (_ A) /\ A (. (B vH C))) -> (B vH C) (_ (B vH x))
52		chub1t 9345	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((B e. CH /\ C e. CH) -> B (_ (B vH C))
53	52	3adant2 796	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((B e. CH /\ x e. CH /\ C e. CH) -> B (_ (B vH C))
54	53, 27	anim12i 333	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((B e. CH /\ x e. CH /\ C e. CH) /\ ((x (_ A /\ -. B (_ A) /\ A (. (B vH C))) -> (B (_ (B vH C) /\ x (_ (B vH C)))
55		chlubt 9347	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((B e. CH /\ x e. CH /\ (B vH C) e. CH) -> ((B (_ (B vH C) /\ x (_ (B vH C)) <-> (B vH x) (_ (B vH C)))
56		chjclt 9244	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((B e. CH /\ C e. CH) -> (B vH C) e. CH)
57	56	3adant2 796	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((B e. CH /\ x e. CH /\ C e. CH) -> (B vH C) e. CH)
58	55, 57	syl3dan3 868	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((B e. CH /\ x e. CH /\ C e. CH) -> ((B (_ (B vH C) /\ x (_ (B vH C)) <-> (B vH x) (_ (B vH C)))
59	58