Theorem atcvatlem 5770

Description: Lemma for atcvat 5771.

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 5766	. . . . . . . . . . . . . . . . 17 |- ((x e. Atoms /\ B e. Atoms) -> (-. x = B <-> (x i^i B) = 0H))
2		sseq1 1521	. . . . . . . . . . . . . . . . . . . . 21 |- (x = B -> (x (_ A <-> B (_ A))
3	2	biimpcd 137	. . . . . . . . . . . . . . . . . . . 20 |- (x (_ A -> (x = B -> B (_ A))
4	3	con3d 87	. . . . . . . . . . . . . . . . . . 19 |- (x (_ A -> (-. B (_ A -> -. x = B))
5	4	imp 277	. . . . . . . . . . . . . . . . . 18 |- ((x (_ A /\ -. B (_ A) -> -. x = B)
6	5	adantrl 311	. . . . . . . . . . . . . . . . 17 |- ((x (_ A /\ (A (. (B vH C) /\ -. B (_ A)) -> -. x = B)
7	1, 6	syl5bi 183	. . . . . . . . . . . . . . . 16 |- ((x e. Atoms /\ B e. Atoms) -> ((x (_ A /\ (A (. (B vH C) /\ -. B (_ A)) -> (x i^i B) = 0H))
8		cvp 5764	. . . . . . . . . . . . . . . . . 18 |- ((x e. CH /\ B e. Atoms) -> ((x i^i B) = 0H <-> x <o (x vH B)))
9		chjcomt 5423	. . . . . . . . . . . . . . . . . . . 20 |- ((x e. CH /\ B e. CH) -> (x vH B) = (B vH x))
10		atelch 5742	. . . . . . . . . . . . . . . . . . . 20 |- (B e. Atoms -> B e. CH)
11	9, 10	sylan2 346	. . . . . . . . . . . . . . . . . . 19 |- ((x e. CH /\ B e. Atoms) -> (x vH B) = (B vH x))
12	11	breq2d 2072	. . . . . . . . . . . . . . . . . 18 |- ((x e. CH /\ B e. Atoms) -> (x <o (x vH B) <-> x <o (B vH x)))
13	8, 12	bitrd 406	. . . . . . . . . . . . . . . . 17 |- ((x e. CH /\ B e. Atoms) -> ((x i^i B) = 0H <-> x <o (B vH x)))
14		atelch 5742	. . . . . . . . . . . . . . . . 17 |- (x e. Atoms -> x e. CH)
15	13, 14	sylan 343	. . . . . . . . . . . . . . . 16 |- ((x e. Atoms /\ B e. Atoms) -> ((x i^i B) = 0H <-> x <o (B vH x)))
16	7, 15	sylibd 177	. . . . . . . . . . . . . . 15 |- ((x e. Atoms /\ B e. Atoms) -> ((x (_ A /\ (A (. (B vH C) /\ -. B (_ A)) -> x <o (B vH x)))
17	16	ancoms 334	. . . . . . . . . . . . . 14 |- ((B e. Atoms /\ x e. Atoms) -> ((x (_ A /\ (A (. (B vH C) /\ -. B (_ A)) -> x <o (B vH x)))
18	17	adantlr 310	. . . . . . . . . . . . 13 |- (((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 277	. . . . . . . . . . . 12 |- ((((B e. Atoms /\ C e. Atoms) /\ x e. Atoms) /\ (x (_ A /\ (A (. (B vH C) /\ -. B (_ A))) -> x <o (B vH x))
20		chub1t 5424	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((B e. CH /\ x e. CH) -> B (_ (B vH x))
21	20, 10, 14	syl2an 349	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((B e. Atoms /\ x e. Atoms) -> B (_ (B vH x))
22	21	3adant3 599	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((B e. Atoms /\ x e. Atoms /\ C e. Atoms) -> B (_ (B vH x))
23	22	adantr 306	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((B e. Atoms /\ x e. Atoms /\ C e. Atoms) /\ ((x (_ A /\ -. B (_ A) /\ A (. (B vH C))) -> B (_ (B vH x))
24		sstr 1511	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((x (_ A /\ A (_ (B vH C)) -> x (_ (B vH C))
25		pssss 1567	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (A (. (B vH C) -> A (_ (B vH C))
26	24, 25	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x (_ A /\ A (. (B vH C)) -> x (_ (B vH C))
27	26	adantlr 310	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((x (_ A /\ -. B (_ A) /\ A (. (B vH C)) -> x (_ (B vH C))
28	27	adantl 305	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((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 183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((x e. Atoms /\ B e. Atoms) -> ((x (_ A /\ -. B (_ A) -> (x i^i B) = 0H))
30	29	ancoms 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((B e. Atoms /\ x e. Atoms) -> ((x (_ A /\ -. B (_ A) -> (x i^i B) = 0H))
31	30	3adant3 599	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((B e. Atoms /\ x e. Atoms /\ C e. Atoms) -> ((x (_ A /\ -. B (_ A) -> (x i^i B) = 0H))
32	31	imp 277	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((B e. Atoms /\ x e. Atoms /\ C e. Atoms) /\ (x (_ A /\ -. B (_ A)) -> (x i^i B) = 0H)
33		incom 1636	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (B i^i x) = (x i^i B)
34	32, 33	syl5eq 1136	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((B e. Atoms /\ x e. Atoms /\ C e. Atoms) /\ (x (_ A /\ -. B (_ A)) -> (B i^i x) = 0H)
35	34	adantrr 312	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((B e. Atoms /\ x e. Atoms /\ C e. Atoms) /\ ((x (_ A /\ -. B (_ A) /\ A (. (B vH C))) -> (B i^i x) = 0H)
36		atexch 5769	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((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 619	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((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 306	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((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 526	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((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 236	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((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 594	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((B e. CH /\ x e. CH /\ C e. CH) -> B e. CH)
42		3simp3 596	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((B e. CH /\ x e. CH /\ C e. CH) -> C e. CH)
43		chjclt 5330	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((B e. CH /\ x e. CH) -> (B vH x) e. CH)
44	43	3adant3 599	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((B e. CH /\ x e. CH /\ C e. CH) -> (B vH x) e. CH)
45	41, 42, 44	3jca 604	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((B e. CH /\ x e. CH /\ C e. CH) -> (B e. CH /\ C e. CH /\ (B vH x) e. CH))
46		atelch 5742	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (C e. Atoms -> C e. CH)
47	45, 10, 14, 46	syl3an 628	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((B e. Atoms /\ x e. Atoms /\ C e. Atoms) -> (B e. CH /\ C e. CH /\ (B vH x) e. CH))
48		chlubt 5426	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((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 12	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((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 306	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((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 170	. . . . . . . . . . . . . . . . . . . . . 22 |- (((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 5424	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((B e. CH /\ C e. CH) -> B (_ (B vH C))
53	52	3adant2 598	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((B e. CH /\ x e. CH /\ C e. CH) -> B (_ (B vH C))
54	53, 27	anim12i 268	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((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 5426	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((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		3simp2 595	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((B e. CH /\ x e. CH /\ C e. CH) -> x e. CH)
57		chjclt 5330	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((B e. CH /\ C e. CH) -> (B vH C) e. CH)
58	57	3adant2 598	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((B e. CH /\ x e. CH /\ C e. CH) -> (B vH C) e. CH)
59	55, 41, 56, 58	syl3anc 629	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((B e. CH /\ x e. CH /\ C e. CH) -> ((B (_ (B vH C) /\ x (_ (B vH C)) <-> (B vH x) (_ (B vH C)))
60	59	adantr 306	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((B e. CH /\ x e. CH /\ C e. CH) /\ ((x (_ A /\ -. B (_ A) <