Theorem atcvat3 10323

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	. . . . . . . . . . 11 |- A e. CH
2		chcv1t 10282	. . . . . . . . . . 11 |- ((A e. CH /\ C e. Atoms) -> (-. C (_ A <-> A <o (A vH C)))
3	1, 2	mpan 695	. . . . . . . . . 10 |- (C e. Atoms -> (-. C (_ A <-> A <o (A vH C)))
4	3	biimpa 416	. . . . . . . . 9 |- ((C e. Atoms /\ -. C (_ A) -> A <o (A vH C))
5	4	ad2ant2lr 410	. . . . . . . 8 |- (((B e. Atoms /\ C e. Atoms) /\ (-. C (_ A /\ B (_ (A vH C))) -> A <o (A vH C))
6		chjcomt 9429	. . . . . . . . . . . . . . . . 17 |- ((B e. CH /\ C e. CH) -> (B vH C) = (C vH B))
7	6	opreq2d 3976	. . . . . . . . . . . . . . . 16 |- ((B e. CH /\ C e. CH) -> (A vH (B vH C)) = (A vH (C vH B)))
8		chjasst 9456	. . . . . . . . . . . . . . . . . 18 |- ((A e. CH /\ C e. CH /\ B e. CH) -> ((A vH C) vH B) = (A vH (C vH B)))
9	1, 8	mp3an1 903	. . . . . . . . . . . . . . . . 17 |- ((C e. CH /\ B e. CH) -> ((A vH C) vH B) = (A vH (C vH B)))
10	9	ancoms 436	. . . . . . . . . . . . . . . 16 |- ((B e. CH /\ C e. CH) -> ((A vH C) vH B) = (A vH (C vH B)))
11	7, 10	eqtr4d 1510	. . . . . . . . . . . . . . 15 |- ((B e. CH /\ C e. CH) -> (A vH (B vH C)) = ((A vH C) vH B))
12	11	adantr 389	. . . . . . . . . . . . . 14 |- (((B e. CH /\ C e. CH) /\ B (_ (A vH C)) -> (A vH (B vH C)) = ((A vH C) vH B))
13		chlej2t 9434	. . . . . . . . . . . . . . . . 17 |- (((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)))
14	13	ex 373	. . . . . . . . . . . . . . . 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 319	. . . . . . . . . . . . . . . 16 |- ((B e. CH /\ C e. CH) -> B e. CH)
16		chjclt 9329	. . . . . . . . . . . . . . . . . 18 |- ((A e. CH /\ C e. CH) -> (A vH C) e. CH)
17	1, 16	mpan 695	. . . . . . . . . . . . . . . . 17 |- (C e. CH -> (A vH C) e. CH)
18	17	adantl 388	. . . . . . . . . . . . . . . 16 |- ((B e. CH /\ C e. CH) -> (A vH C) e. CH)
19	14, 15, 18, 18	syl3anc 858	. . . . . . . . . . . . . . 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 350	. . . . . . . . . . . . . 14 |- (((B e. CH /\ C e. CH) /\ B (_ (A vH C)) -> ((A vH C) vH B) (_ ((A vH C) vH (A vH C)))
21	12, 20	eqsstrd 2095	. . . . . . . . . . . . 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 9443	. . . . . . . . . . . . . . 15 |- ((A vH C) e. CH -> ((A vH C) vH (A vH C)) = (A vH C))
23	17, 22	syl 10	. . . . . . . . . . . . . 14 |- (C e. CH -> ((A vH C) vH (A vH C)) = (A vH C))
24	23	ad2antlr 405	. . . . . . . . . . . . 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 2097	. . . . . . . . . . . 12 |- (((B e. CH /\ C e. CH) /\ B (_ (A vH C)) -> (A vH (B vH C)) (_ (A vH C))
26		chlej2t 9434	. . . . . . . . . . . . . . 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	mp3anl3 912	. . . . . . . . . . . . . 14 |- (((C e. CH /\ (B vH C) e. CH) /\ C (_ (B vH C)) -> (A vH C) (_ (A vH (B vH C)))
28		pm3.27 323	. . . . . . . . . . . . . . 15 |- ((B e. CH /\ C e. CH) -> C e. CH)
29		chjclt 9329	. . . . . . . . . . . . . . 15 |- ((B e. CH /\ C e. CH) -> (B vH C) e. CH)
30	28, 29	jca 288	. . . . . . . . . . . . . 14 |- ((B e. CH /\ C e. CH) -> (C e. CH /\ (B vH C) e. CH))
31		chub2t 9431	. . . . . . . . . . . . . . 15 |- ((C e. CH /\ B e. CH) -> C (_ (B vH C))
32	31	ancoms 436	. . . . . . . . . . . . . 14 |- ((B e. CH /\ C e. CH) -> C (_ (B vH C))
33	27, 30, 32	sylanc 471	. . . . . . . . . . . . 13 |- ((B e. CH /\ C e. CH) -> (A vH C) (_ (A vH (B vH C)))
34	33	adantr 389	. . . . . . . . . . . 12 |- (((B e. CH /\ C e. CH) /\ B (_ (A vH C)) -> (A vH C) (_ (A vH (B vH C)))
35	25, 34	eqssd 2079	. . . . . . . . . . 11 |- (((B e. CH /\ C e. CH) /\ B (_ (A vH C)) -> (A vH (B vH C)) = (A vH C))
36		atelch 10271	. . . . . . . . . . . 12 |- (B e. Atoms -> B e. CH)
37		atelch 10271	. . . . . . . . . . . 12 |- (C e. Atoms -> C e. CH)
38	36, 37	anim12i 333	. . . . . . . . . . 11 |- ((B e. Atoms /\ C e. Atoms) -> (B e. CH /\ C e. CH))
39	35, 38	sylan 448	. . . . . . . . . 10 |- (((B e. Atoms /\ C e. Atoms) /\ B (_ (A vH C)) -> (A vH (B vH C)) = (A vH C))
40	39	breq2d 2630	. . . . . . . . 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 394	. . . . . . . 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	5, 41	mpbird 196	. . . . . . 7 |- (((B e. Atoms /\ C e. Atoms) /\ (-. C (_ A /\ B (_ (A vH C))) -> A <o (A vH (B vH C)))
43	42	ex 373	. . . . . 6 |- ((B e. Atoms /\ C e. Atoms) -> ((-. C (_ A /\ B (_ (A vH C)) -> A <o (A vH (B vH C))))
44	29, 1	jctil 292	. . . . . . . 8 |- ((B e. CH /\ C e. CH) -> (A e. CH /\ (B vH C) e. CH))
45	44, 36, 37	syl2an 454	. . . . . . 7 |- ((B e. Atoms /\ C e. Atoms) -> (A e. CH /\ (B vH C) e. CH))
46		cvexcht 10301	. . . . . . 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 10	. . . . . 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 204	. . . . 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 389	. . . 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 10316	. . . . . . 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 9422	. . . . . . . . 9 |- ((A e. CH /\ (B vH C) e. CH) -> (A i^i (B vH C)) e. CH)
52	44, 51	syl 10	. . . . . . . 8 |- ((B e. CH /\ C e. CH) -> (A i^i (B vH C)) e. CH)
53	52, 36, 37	syl2an 454	. . . . . . 7 |- ((B e. Atoms /\ C e. Atoms) -> (A i^i (B vH C)) e. CH)
54		pm3.26 319	. . . . . . 7 |- ((B e. Atoms /\ C e. Atoms) -> B e. Atoms)
55		pm3.27 323	. . . . . . 7 |- ((B e. Atoms /\ C e. Atoms) -> C e. Atoms)
56	50, 53, 54, 55	syl3anc 858	. . . . . 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 375	. . . . 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 350	. . . 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