Theorem atcvat3 5774

Description: A condition implying that a certain lattice element is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68.

Hypothesis

Ref	Expression
atcvat3.1	|- A e. CH

Assertion

Ref	Expression
atcvat3	|- ((B e. Atoms /\ C e. Atoms) -> (((-. B = C /\ -. C (_ A) /\ B (_ (A vH C)) -> (A i^i (B vH C)) e. Atoms))

Proof of Theorem atcvat3

Step	Hyp	Ref	Expression
1		atcvat3.1	. . . . . . . . . . . 12 |- A e. CH
2		chcv1t 5751	. . . . . . . . . . . 12 |- ((A e. CH /\ C e. Atoms) -> (-. C (_ A <-> A <o (A vH C)))
3	1, 2	mpan 518	. . . . . . . . . . 11 |- (C e. Atoms -> (-. C (_ A <-> A <o (A vH C)))
4	3	biimpa 324	. . . . . . . . . 10 |- ((C e. Atoms /\ -. C (_ A) -> A <o (A vH C))
5	4	adantll 309	. . . . . . . . 9 |- (((B e. Atoms /\ C e. Atoms) /\ -. C (_ A) -> A <o (A vH C))
6	5	adantrr 312	. . . . . . . 8 |- (((B e. Atoms /\ C e. Atoms) /\ (-. C (_ A /\ B (_ (A vH C))) -> A <o (A vH C))
7		chjcomt 5423	. . . . . . . . . . . . . . . . 17 |- ((B e. CH /\ C e. CH) -> (B vH C) = (C vH B))
8	7	opreq2d 3013	. . . . . . . . . . . . . . . 16 |- ((B e. CH /\ C e. CH) -> (A vH (B vH C)) = (A vH (C vH B)))
9		chjasst 5446	. . . . . . . . . . . . . . . . . 18 |- ((A e. CH /\ C e. CH /\ B e. CH) -> ((A vH C) vH B) = (A vH (C vH B)))
10	1, 9	mp3an1 639	. . . . . . . . . . . . . . . . 17 |- ((C e. CH /\ B e. CH) -> ((A vH C) vH B) = (A vH (C vH B)))
11	10	ancoms 334	. . . . . . . . . . . . . . . 16 |- ((B e. CH /\ C e. CH) -> ((A vH C) vH B) = (A vH (C vH B)))
12	8, 11	eqtr4d 1131	. . . . . . . . . . . . . . 15 |- ((B e. CH /\ C e. CH) -> (A vH (B vH C)) = ((A vH C) vH B))
13	12	adantr 306	. . . . . . . . . . . . . 14 |- (((B e. CH /\ C e. CH) /\ B (_ (A vH C)) -> (A vH (B vH C)) = ((A vH C) vH B))
14		chlej2t 5428	. . . . . . . . . . . . . . . 16 |- ((B e. CH /\ (A vH C) e. CH /\ (A vH C) e. CH) -> (B (_ (A vH C) -> ((A vH C) vH B) (_ ((A vH C) vH (A vH C))))
15		pm3.26 256	. . . . . . . . . . . . . . . 16 |- ((B e. CH /\ C e. CH) -> B e. CH)
16		chjclt 5330	. . . . . . . . . . . . . . . . . 18 |- ((A e. CH /\ C e. CH) -> (A vH C) e. CH)
17	1, 16	mpan 518	. . . . . . . . . . . . . . . . 17 |- (C e. CH -> (A vH C) e. CH)
18	17	adantl 305	. . . . . . . . . . . . . . . 16 |- ((B e. CH /\ C e. CH) -> (A vH C) e. CH)
19	14, 15, 18, 18	syl3anc 629	. . . . . . . . . . . . . . 15 |- ((B e. CH /\ C e. CH) -> (B (_ (A vH C) -> ((A vH C) vH B) (_ ((A vH C) vH (A vH C))))
20	19	imp 277	. . . . . . . . . . . . . 14 |- (((B e. CH /\ C e. CH) /\ B (_ (A vH C)) -> ((A vH C) vH B) (_ ((A vH C) vH (A vH C)))
21	13, 20	eqsstrd 1534	. . . . . . . . . . . . 13 |- (((B e. CH /\ C e. CH) /\ B (_ (A vH C)) -> (A vH (B vH C)) (_ ((A vH C) vH (A vH C)))
22		chjidmt 5436	. . . . . . . . . . . . . . 15 |- ((A vH C) e. CH -> ((A vH C) vH (A vH C)) = (A vH C))
23	17, 22	syl 12	. . . . . . . . . . . . . 14 |- (C e. CH -> ((A vH C) vH (A vH C)) = (A vH C))
24	23	ad2antlr 321	. . . . . . . . . . . . 13 |- (((B e. CH /\ C e. CH) /\ B (_ (A vH C)) -> ((A vH C) vH (A vH C)) = (A vH C))
25	21, 24	sseqtrd 1536	. . . . . . . . . . . 12 |- (((B e. CH /\ C e. CH) /\ B (_ (A vH C)) -> (A vH (B vH C)) (_ (A vH C))
26		chlej2t 5428	. . . . . . . . . . . . . . 15 |- ((C e. CH /\ (B vH C) e. CH /\ A e. CH) -> (C (_ (B vH C) -> (A vH C) (_ (A vH (B vH C))))
27	1, 26	mp3an3 641	. . . . . . . . . . . . . 14 |- ((C e. CH /\ (B vH C) e. CH) -> (C (_ (B vH C) -> (A vH C) (_ (A vH (B vH C))))
28		pm3.27 260	. . . . . . . . . . . . . . 15 |- ((B e. CH /\ C e. CH) -> C e. CH)
29		chjclt 5330	. . . . . . . . . . . . . . 15 |- ((B e. CH /\ C e. CH) -> (B vH C) e. CH)
30	28, 29	jca 236	. . . . . . . . . . . . . 14 |- ((B e. CH /\ C e. CH) -> (C e. CH /\ (B vH C) e. CH))
31		chub2t 5425	. . . . . . . . . . . . . . 15 |- ((C e. CH /\ B e. CH) -> C (_ (B vH C))
32	31	ancoms 334	. . . . . . . . . . . . . 14 |- ((B e. CH /\ C e. CH) -> C (_ (B vH C))
33	27, 30, 32	sylc 62	. . . . . . . . . . . . 13 |- ((B e. CH /\ C e. CH) -> (A vH C) (_ (A vH (B vH C)))
34	33	adantr 306	. . . . . . . . . . . 12 |- (((B e. CH /\ C e. CH) /\ B (_ (A vH C)) -> (A vH C) (_ (A vH (B vH C)))
35	25, 34	eqssd 1518	. . . . . . . . . . 11 |- (((B e. CH /\ C e. CH) /\ B (_ (A vH C)) -> (A vH (B vH C)) = (A vH C))
36		atelch 5742	. . . . . . . . . . . 12 |- (B e. Atoms -> B e. CH)
37		atelch 5742	. . . . . . . . . . . 12 |- (C e. Atoms -> C e. CH)
38	36, 37	anim12i 268	. . . . . . . . . . 11 |- ((B e. Atoms /\ C e. Atoms) -> (B e. CH /\ C e. CH))
39	35, 38	sylan 343	. . . . . . . . . 10 |- (((B e. Atoms /\ C e. Atoms) /\ B (_ (A vH C)) -> (A vH (B vH C)) = (A vH C))
40	39	breq2d 2072	. . . . . . . . 9 |- (((B e. Atoms /\ C e. Atoms) /\ B (_ (A vH C)) -> (A <o (A vH (B vH C)) <-> A <o (A vH C)))
41	40	adantrl 311	. . . . . . . 8 |- (((B e. Atoms /\ C e. Atoms) /\ (-. C (_ A /\ B (_ (A vH C))) -> (A <o (A vH (B vH C)) <-> A <o (A vH C)))
42	6, 41	mpbird 171	. . . . . . 7 |- (((B e. Atoms /\ C e. Atoms) /\ (-. C (_ A /\ B (_ (A vH C))) -> A <o (A vH (B vH C)))
43	42	exp 291	. . . . . 6 |- ((B e. Atoms /\ C e. Atoms) -> ((-. C (_ A /\ B (_ (A vH C)) -> A <o (A vH (B vH C))))
44	29, 1	jctil 240	. . . . . . . 8 |- ((B e. CH /\ C e. CH) -> (A e. CH /\ (B vH C) e. CH))
45	44, 36, 37	syl2an 349	. . . . . . 7 |- ((B e. Atoms /\ C e. Atoms) -> (A e. CH /\ (B vH C) e. CH))
46		cvexcht 5763	. . . . . . 7 |- ((A e. CH /\ (B vH C) e. CH) -> ((A i^i (B vH C)) <o (B vH C) <-> A <o (A vH (B vH C))))
47	45, 46	syl 12	. . . . . 6 |- ((B e. Atoms /\ C e. Atoms) -> ((A i^i (B vH C)) <o (B vH C) <-> A <o (A vH (B vH C))))
48	43, 47	sylibrd 179	. . . . 5 |- ((B e. Atoms /\ C e. Atoms) -> ((-. C (_ A /\ B (_ (A vH C)) -> (A i^i (B vH C)) <o (B vH C)))
49	48	adantr 306	. . . 4 |- (((B e. Atoms /\ C e. Atoms) /\ -. B = C) -> ((-. C (_ A /\ B (_ (A vH C)) -> (A i^i (B vH C)) <o (B vH C)))
50		atcvat2t 5773	. . . . . . 7 |- (((A i^i (B vH C)) e. CH /\ B e. Atoms /\ C e. Atoms) -> ((-. B = C /\ (A i^i (B vH C)) <o (B vH C)) -> (A i^i (B vH C)) e. Atoms))
51		chinclt 5416	. . . . . . . . 9 |- ((A e. CH /\ (B vH C) e. CH) -> (A i^i (B vH C)) e. CH)
52	44, 51	syl 12	. . . . . . . 8 |- ((B e. CH /\ C e. CH) -> (A i^i (B vH C)) e. CH)
53	52, 36, 37	syl2an 349	. . . . . . 7 |- ((B e. Atoms /\ C e. Atoms) -> (A i^i (B vH C)) e. CH)
54		pm3.26 256	. . . . . . 7 |- ((B e. Atoms /\ C e. Atoms) -> B e. Atoms)
55		pm3.27 260	. . . . . . 7 |- ((B e. Atoms /\ C e. Atoms) -> C e. Atoms)
56	50, 53, 54, 55	syl3anc 629	. . . . . 6 |- ((B e. Atoms /\ C e. Atoms) -> ((-. B = C /\ (A i^i (B vH C)) <o (B vH C)) -> (A i^i (B vH C)) e. Atoms))
57	56	exp3a 292	. . . . 5 |- ((B e. Atoms /\ C e. Atoms) -> (-. B = C -> ((A i^i (B vH C)) <o (B vH C) -> (A i^i (B vH C)) e. Atoms)))
58	57	imp 277	. . . 4 |- (((B e. Atoms /\ C e. Atoms) /\ -. B = C) -> ((A i^i (B vH C)) <o (B vH C) -> (A i^i (B vH C)) e. Atoms))
59	49, 58	syld 27	. . 3 |- (((B e. Atoms /\ C e. Atoms) /\ -. B = C) -> ((-. C (_ A /\ B (_ (A vH C)) -> (A i^i (B vH C)) e. Atoms))
60	59	exp4b 296	. 2 |- ((B e. Atoms /\ C e. Atoms) -> (-. B = C -> (-. C (_ A -> (B (_ (A vH C) -> (A i^i (B vH C)) e. Atoms))))
61	60	imp4c 284	1 |- ((B e. Atoms /\ C e. Atoms) -> (((-. B = C