Metamath Proof Explorer

Theorem atcvat3i

Description: A condition implying that a certain lattice element is an atom. Part of Lemma 3.2.20 of PtakPulmannova p. 68. (Contributed by NM, 2-Jul-2004) (New usage is discouraged.)

Ref Expression
Hypothesis atcvat3.1 
|- A e. CH
Assertion atcvat3i 
|- ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( ( -. B = C /\ -. C C_ A ) /\ B C_ ( A vH C ) ) -> ( A i^i ( B vH C ) ) e. HAtoms ) )

Proof

Step Hyp Ref Expression
1 atcvat3.1 
 |-  A e. CH
2 chcv1 
 |-  ( ( A e. CH /\ C e. HAtoms ) -> ( -. C C_ A <-> A
3 1 2 mpan 
 |-  ( C e. HAtoms -> ( -. C C_ A <-> A
4 3 biimpa 
 |-  ( ( C e. HAtoms /\ -. C C_ A ) -> A
5 4 ad2ant2lr 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ ( -. C C_ A /\ B C_ ( A vH C ) ) ) -> A
6 atelch 
 |-  ( B e. HAtoms -> B e. CH )
7 atelch 
 |-  ( C e. HAtoms -> C e. CH )
8 6 7 anim12i 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( B e. CH /\ C e. CH ) )
9 chjcom 
 |-  ( ( B e. CH /\ C e. CH ) -> ( B vH C ) = ( C vH B ) )
10 9 oveq2d 
 |-  ( ( B e. CH /\ C e. CH ) -> ( A vH ( B vH C ) ) = ( A vH ( C vH B ) ) )
11 chjass 
 |-  ( ( A e. CH /\ C e. CH /\ B e. CH ) -> ( ( A vH C ) vH B ) = ( A vH ( C vH B ) ) )
12 1 11 mp3an1 
 |-  ( ( C e. CH /\ B e. CH ) -> ( ( A vH C ) vH B ) = ( A vH ( C vH B ) ) )
13 12 ancoms 
 |-  ( ( B e. CH /\ C e. CH ) -> ( ( A vH C ) vH B ) = ( A vH ( C vH B ) ) )
14 10 13 eqtr4d 
 |-  ( ( B e. CH /\ C e. CH ) -> ( A vH ( B vH C ) ) = ( ( A vH C ) vH B ) )
15 14 adantr 
 |-  ( ( ( B e. CH /\ C e. CH ) /\ B C_ ( A vH C ) ) -> ( A vH ( B vH C ) ) = ( ( A vH C ) vH B ) )
16 simpl 
 |-  ( ( B e. CH /\ C e. CH ) -> B e. CH )
17 chjcl 
 |-  ( ( A e. CH /\ C e. CH ) -> ( A vH C ) e. CH )
18 1 17 mpan 
 |-  ( C e. CH -> ( A vH C ) e. CH )
19 18 adantl 
 |-  ( ( B e. CH /\ C e. CH ) -> ( A vH C ) e. CH )
20 chlej2 
 |-  ( ( ( B e. CH /\ ( A vH C ) e. CH /\ ( A vH C ) e. CH ) /\ B C_ ( A vH C ) ) -> ( ( A vH C ) vH B ) C_ ( ( A vH C ) vH ( A vH C ) ) )
21 20 ex 
 |-  ( ( B e. CH /\ ( A vH C ) e. CH /\ ( A vH C ) e. CH ) -> ( B C_ ( A vH C ) -> ( ( A vH C ) vH B ) C_ ( ( A vH C ) vH ( A vH C ) ) ) )
22 16 19 19 21 syl3anc 
 |-  ( ( B e. CH /\ C e. CH ) -> ( B C_ ( A vH C ) -> ( ( A vH C ) vH B ) C_ ( ( A vH C ) vH ( A vH C ) ) ) )
23 22 imp 
 |-  ( ( ( B e. CH /\ C e. CH ) /\ B C_ ( A vH C ) ) -> ( ( A vH C ) vH B ) C_ ( ( A vH C ) vH ( A vH C ) ) )
24 15 23 eqsstrd 
 |-  ( ( ( B e. CH /\ C e. CH ) /\ B C_ ( A vH C ) ) -> ( A vH ( B vH C ) ) C_ ( ( A vH C ) vH ( A vH C ) ) )
25 chjidm 
 |-  ( ( A vH C ) e. CH -> ( ( A vH C ) vH ( A vH C ) ) = ( A vH C ) )
26 18 25 syl 
 |-  ( C e. CH -> ( ( A vH C ) vH ( A vH C ) ) = ( A vH C ) )
27 26 ad2antlr 
 |-  ( ( ( B e. CH /\ C e. CH ) /\ B C_ ( A vH C ) ) -> ( ( A vH C ) vH ( A vH C ) ) = ( A vH C ) )
28 24 27 sseqtrd 
 |-  ( ( ( B e. CH /\ C e. CH ) /\ B C_ ( A vH C ) ) -> ( A vH ( B vH C ) ) C_ ( A vH C ) )
29 simpr 
 |-  ( ( B e. CH /\ C e. CH ) -> C e. CH )
30 chjcl 
 |-  ( ( B e. CH /\ C e. CH ) -> ( B vH C ) e. CH )
31 chub2 
 |-  ( ( C e. CH /\ B e. CH ) -> C C_ ( B vH C ) )
32 31 ancoms 
 |-  ( ( B e. CH /\ C e. CH ) -> C C_ ( B vH C ) )
33 chlej2 
 |-  ( ( ( C e. CH /\ ( B vH C ) e. CH /\ A e. CH ) /\ C C_ ( B vH C ) ) -> ( A vH C ) C_ ( A vH ( B vH C ) ) )
34 1 33 mp3anl3 
 |-  ( ( ( C e. CH /\ ( B vH C ) e. CH ) /\ C C_ ( B vH C ) ) -> ( A vH C ) C_ ( A vH ( B vH C ) ) )
35 29 30 32 34 syl21anc 
 |-  ( ( B e. CH /\ C e. CH ) -> ( A vH C ) C_ ( A vH ( B vH C ) ) )
36 35 adantr 
 |-  ( ( ( B e. CH /\ C e. CH ) /\ B C_ ( A vH C ) ) -> ( A vH C ) C_ ( A vH ( B vH C ) ) )
37 28 36 eqssd 
 |-  ( ( ( B e. CH /\ C e. CH ) /\ B C_ ( A vH C ) ) -> ( A vH ( B vH C ) ) = ( A vH C ) )
38 8 37 sylan 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ B C_ ( A vH C ) ) -> ( A vH ( B vH C ) ) = ( A vH C ) )
39 38 breq2d 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ B C_ ( A vH C ) ) -> ( A  A
40 39 adantrl 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ ( -. C C_ A /\ B C_ ( A vH C ) ) ) -> ( A  A
41 5 40 mpbird 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ ( -. C C_ A /\ B C_ ( A vH C ) ) ) -> A
42 41 ex 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( -. C C_ A /\ B C_ ( A vH C ) ) -> A
43 30 1 jctil 
 |-  ( ( B e. CH /\ C e. CH ) -> ( A e. CH /\ ( B vH C ) e. CH ) )
44 6 7 43 syl2an 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( A e. CH /\ ( B vH C ) e. CH ) )
45 cvexch 
 |-  ( ( A e. CH /\ ( B vH C ) e. CH ) -> ( ( A i^i ( B vH C ) )  A
46 44 45 syl 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( A i^i ( B vH C ) )  A
47 42 46 sylibrd 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( -. C C_ A /\ B C_ ( A vH C ) ) -> ( A i^i ( B vH C ) )
48 47 adantr 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ -. B = C ) -> ( ( -. C C_ A /\ B C_ ( A vH C ) ) -> ( A i^i ( B vH C ) )
49 chincl 
 |-  ( ( A e. CH /\ ( B vH C ) e. CH ) -> ( A i^i ( B vH C ) ) e. CH )
50 1 30 49 sylancr 
 |-  ( ( B e. CH /\ C e. CH ) -> ( A i^i ( B vH C ) ) e. CH )
51 6 7 50 syl2an 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( A i^i ( B vH C ) ) e. CH )
52 simpl 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> B e. HAtoms )
53 simpr 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> C e. HAtoms )
54 atcvat2 
 |-  ( ( ( A i^i ( B vH C ) ) e. CH /\ B e. HAtoms /\ C e. HAtoms ) -> ( ( -. B = C /\ ( A i^i ( B vH C ) )  ( A i^i ( B vH C ) ) e. HAtoms ) )
55 51 52 53 54 syl3anc 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( -. B = C /\ ( A i^i ( B vH C ) )  ( A i^i ( B vH C ) ) e. HAtoms ) )
56 55 expdimp 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ -. B = C ) -> ( ( A i^i ( B vH C ) )  ( A i^i ( B vH C ) ) e. HAtoms ) )
57 48 56 syld 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ -. B = C ) -> ( ( -. C C_ A /\ B C_ ( A vH C ) ) -> ( A i^i ( B vH C ) ) e. HAtoms ) )
58 57 exp4b 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( -. B = C -> ( -. C C_ A -> ( B C_ ( A vH C ) -> ( A i^i ( B vH C ) ) e. HAtoms ) ) ) )
59 58 imp4c 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( ( -. B = C /\ -. C C_ A ) /\ B C_ ( A vH C ) ) -> ( A i^i ( B vH C ) ) e. HAtoms ) )