Metamath Proof Explorer

Theorem atcvatlem

Description: Lemma for atcvati . (Contributed by NM, 27-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypothesis atoml.1 
|- A e. CH
Assertion atcvatlem 
|- ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ ( A =/= 0H /\ A C. ( B vH C ) ) ) -> ( -. B C_ A -> A e. HAtoms ) )

Proof

Step Hyp Ref Expression
1 atoml.1 
 |-  A e. CH
2 1 hatomici 
 |-  ( A =/= 0H -> E. x e. HAtoms x C_ A )
3 nssne2 
 |-  ( ( x C_ A /\ -. B C_ A ) -> x =/= B )
4 3 adantrl 
 |-  ( ( x C_ A /\ ( A C. ( B vH C ) /\ -. B C_ A ) ) -> x =/= B )
5 atnemeq0 
 |-  ( ( x e. HAtoms /\ B e. HAtoms ) -> ( x =/= B <-> ( x i^i B ) = 0H ) )
6 4 5 syl5ib 
 |-  ( ( x e. HAtoms /\ B e. HAtoms ) -> ( ( x C_ A /\ ( A C. ( B vH C ) /\ -. B C_ A ) ) -> ( x i^i B ) = 0H ) )
7 atelch 
 |-  ( x e. HAtoms -> x e. CH )
8 cvp 
 |-  ( ( x e. CH /\ B e. HAtoms ) -> ( ( x i^i B ) = 0H <-> x
9 atelch 
 |-  ( B e. HAtoms -> B e. CH )
10 chjcom 
 |-  ( ( x e. CH /\ B e. CH ) -> ( x vH B ) = ( B vH x ) )
11 9 10 sylan2 
 |-  ( ( x e. CH /\ B e. HAtoms ) -> ( x vH B ) = ( B vH x ) )
12 11 breq2d 
 |-  ( ( x e. CH /\ B e. HAtoms ) -> ( x  x
13 8 12 bitrd 
 |-  ( ( x e. CH /\ B e. HAtoms ) -> ( ( x i^i B ) = 0H <-> x
14 7 13 sylan 
 |-  ( ( x e. HAtoms /\ B e. HAtoms ) -> ( ( x i^i B ) = 0H <-> x
15 6 14 sylibd 
 |-  ( ( x e. HAtoms /\ B e. HAtoms ) -> ( ( x C_ A /\ ( A C. ( B vH C ) /\ -. B C_ A ) ) -> x
16 15 ancoms 
 |-  ( ( B e. HAtoms /\ x e. HAtoms ) -> ( ( x C_ A /\ ( A C. ( B vH C ) /\ -. B C_ A ) ) -> x
17 16 adantlr 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ x e. HAtoms ) -> ( ( x C_ A /\ ( A C. ( B vH C ) /\ -. B C_ A ) ) -> x
18 17 imp 
 |-  ( ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ x e. HAtoms ) /\ ( x C_ A /\ ( A C. ( B vH C ) /\ -. B C_ A ) ) ) -> x
19 chub1 
 |-  ( ( B e. CH /\ x e. CH ) -> B C_ ( B vH x ) )
20 9 7 19 syl2an 
 |-  ( ( B e. HAtoms /\ x e. HAtoms ) -> B C_ ( B vH x ) )
21 20 3adant3 
 |-  ( ( B e. HAtoms /\ x e. HAtoms /\ C e. HAtoms ) -> B C_ ( B vH x ) )
22 21 adantr 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms /\ C e. HAtoms ) /\ ( ( x C_ A /\ -. B C_ A ) /\ A C. ( B vH C ) ) ) -> B C_ ( B vH x ) )
23 pssss 
 |-  ( A C. ( B vH C ) -> A C_ ( B vH C ) )
24 sstr 
 |-  ( ( x C_ A /\ A C_ ( B vH C ) ) -> x C_ ( B vH C ) )
25 23 24 sylan2 
 |-  ( ( x C_ A /\ A C. ( B vH C ) ) -> x C_ ( B vH C ) )
26 25 adantlr 
 |-  ( ( ( x C_ A /\ -. B C_ A ) /\ A C. ( B vH C ) ) -> x C_ ( B vH C ) )
27 26 adantl 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms /\ C e. HAtoms ) /\ ( ( x C_ A /\ -. B C_ A ) /\ A C. ( B vH C ) ) ) -> x C_ ( B vH C ) )
28 incom 
 |-  ( B i^i x ) = ( x i^i B )
29 3 5 syl5ib 
 |-  ( ( x e. HAtoms /\ B e. HAtoms ) -> ( ( x C_ A /\ -. B C_ A ) -> ( x i^i B ) = 0H ) )
30 29 ancoms 
 |-  ( ( B e. HAtoms /\ x e. HAtoms ) -> ( ( x C_ A /\ -. B C_ A ) -> ( x i^i B ) = 0H ) )
31 30 3adant3 
 |-  ( ( B e. HAtoms /\ x e. HAtoms /\ C e. HAtoms ) -> ( ( x C_ A /\ -. B C_ A ) -> ( x i^i B ) = 0H ) )
32 31 imp 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms /\ C e. HAtoms ) /\ ( x C_ A /\ -. B C_ A ) ) -> ( x i^i B ) = 0H )
33 28 32 syl5eq 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms /\ C e. HAtoms ) /\ ( x C_ A /\ -. B C_ A ) ) -> ( B i^i x ) = 0H )
34 33 adantrr 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms /\ C e. HAtoms ) /\ ( ( x C_ A /\ -. B C_ A ) /\ A C. ( B vH C ) ) ) -> ( B i^i x ) = 0H )
35 atexch 
 |-  ( ( B e. CH /\ x e. HAtoms /\ C e. HAtoms ) -> ( ( x C_ ( B vH C ) /\ ( B i^i x ) = 0H ) -> C C_ ( B vH x ) ) )
36 9 35 syl3an1 
 |-  ( ( B e. HAtoms /\ x e. HAtoms /\ C e. HAtoms ) -> ( ( x C_ ( B vH C ) /\ ( B i^i x ) = 0H ) -> C C_ ( B vH x ) ) )
37 36 adantr 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms /\ C e. HAtoms ) /\ ( ( x C_ A /\ -. B C_ A ) /\ A C. ( B vH C ) ) ) -> ( ( x C_ ( B vH C ) /\ ( B i^i x ) = 0H ) -> C C_ ( B vH x ) ) )
38 27 34 37 mp2and 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms /\ C e. HAtoms ) /\ ( ( x C_ A /\ -. B C_ A ) /\ A C. ( B vH C ) ) ) -> C C_ ( B vH x ) )
39 atelch 
 |-  ( C e. HAtoms -> C e. CH )
40 simp1 
 |-  ( ( B e. CH /\ x e. CH /\ C e. CH ) -> B e. CH )
41 simp3 
 |-  ( ( B e. CH /\ x e. CH /\ C e. CH ) -> C e. CH )
42 chjcl 
 |-  ( ( B e. CH /\ x e. CH ) -> ( B vH x ) e. CH )
43 42 3adant3 
 |-  ( ( B e. CH /\ x e. CH /\ C e. CH ) -> ( B vH x ) e. CH )
44 40 41 43 3jca 
 |-  ( ( B e. CH /\ x e. CH /\ C e. CH ) -> ( B e. CH /\ C e. CH /\ ( B vH x ) e. CH ) )
45 9 7 39 44 syl3an 
 |-  ( ( B e. HAtoms /\ x e. HAtoms /\ C e. HAtoms ) -> ( B e. CH /\ C e. CH /\ ( B vH x ) e. CH ) )
46 chlub 
 |-  ( ( B e. CH /\ C e. CH /\ ( B vH x ) e. CH ) -> ( ( B C_ ( B vH x ) /\ C C_ ( B vH x ) ) <-> ( B vH C ) C_ ( B vH x ) ) )
47 45 46 syl 
 |-  ( ( B e. HAtoms /\ x e. HAtoms /\ C e. HAtoms ) -> ( ( B C_ ( B vH x ) /\ C C_ ( B vH x ) ) <-> ( B vH C ) C_ ( B vH x ) ) )
48 47 adantr 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms /\ C e. HAtoms ) /\ ( ( x C_ A /\ -. B C_ A ) /\ A C. ( B vH C ) ) ) -> ( ( B C_ ( B vH x ) /\ C C_ ( B vH x ) ) <-> ( B vH C ) C_ ( B vH x ) ) )
49 22 38 48 mpbi2and 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms /\ C e. HAtoms ) /\ ( ( x C_ A /\ -. B C_ A ) /\ A C. ( B vH C ) ) ) -> ( B vH C ) C_ ( B vH x ) )
50 chub1 
 |-  ( ( B e. CH /\ C e. CH ) -> B C_ ( B vH C ) )
51 50 3adant2 
 |-  ( ( B e. CH /\ x e. CH /\ C e. CH ) -> B C_ ( B vH C ) )
52 51 26 anim12i 
 |-  ( ( ( B e. CH /\ x e. CH /\ C e. CH ) /\ ( ( x C_ A /\ -. B C_ A ) /\ A C. ( B vH C ) ) ) -> ( B C_ ( B vH C ) /\ x C_ ( B vH C ) ) )
53 chjcl 
 |-  ( ( B e. CH /\ C e. CH ) -> ( B vH C ) e. CH )
54 53 3adant2 
 |-  ( ( B e. CH /\ x e. CH /\ C e. CH ) -> ( B vH C ) e. CH )
55 chlub 
 |-  ( ( B e. CH /\ x e. CH /\ ( B vH C ) e. CH ) -> ( ( B C_ ( B vH C ) /\ x C_ ( B vH C ) ) <-> ( B vH x ) C_ ( B vH C ) ) )
56 54 55 syld3an3 
 |-  ( ( B e. CH /\ x e. CH /\ C e. CH ) -> ( ( B C_ ( B vH C ) /\ x C_ ( B vH C ) ) <-> ( B vH x ) C_ ( B vH C ) ) )
57 56 adantr 
 |-  ( ( ( B e. CH /\ x e. CH /\ C e. CH ) /\ ( ( x C_ A /\ -. B C_ A ) /\ A C. ( B vH C ) ) ) -> ( ( B C_ ( B vH C ) /\ x C_ ( B vH C ) ) <-> ( B vH x ) C_ ( B vH C ) ) )
58 52 57 mpbid 
 |-  ( ( ( B e. CH /\ x e. CH /\ C e. CH ) /\ ( ( x C_ A /\ -. B C_ A ) /\ A C. ( B vH C ) ) ) -> ( B vH x ) C_ ( B vH C ) )
59 9 7 39 58 syl3anl 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms /\ C e. HAtoms ) /\ ( ( x C_ A /\ -. B C_ A ) /\ A C. ( B vH C ) ) ) -> ( B vH x ) C_ ( B vH C ) )
60 49 59 eqssd 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms /\ C e. HAtoms ) /\ ( ( x C_ A /\ -. B C_ A ) /\ A C. ( B vH C ) ) ) -> ( B vH C ) = ( B vH x ) )
61 60 anassrs 
 |-  ( ( ( ( B e. HAtoms /\ x e. HAtoms /\ C e. HAtoms ) /\ ( x C_ A /\ -. B C_ A ) ) /\ A C. ( B vH C ) ) -> ( B vH C ) = ( B vH x ) )
62 61 psseq2d 
 |-  ( ( ( ( B e. HAtoms /\ x e. HAtoms /\ C e. HAtoms ) /\ ( x C_ A /\ -. B C_ A ) ) /\ A C. ( B vH C ) ) -> ( A C. ( B vH C ) <-> A C. ( B vH x ) ) )
63 62 ex 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms /\ C e. HAtoms ) /\ ( x C_ A /\ -. B C_ A ) ) -> ( A C. ( B vH C ) -> ( A C. ( B vH C ) <-> A C. ( B vH x ) ) ) )
64 63 ibd 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms /\ C e. HAtoms ) /\ ( x C_ A /\ -. B C_ A ) ) -> ( A C. ( B vH C ) -> A C. ( B vH x ) ) )
65 64 exp32 
 |-  ( ( B e. HAtoms /\ x e. HAtoms /\ C e. HAtoms ) -> ( x C_ A -> ( -. B C_ A -> ( A C. ( B vH C ) -> A C. ( B vH x ) ) ) ) )
66 65 3expa 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms ) /\ C e. HAtoms ) -> ( x C_ A -> ( -. B C_ A -> ( A C. ( B vH C ) -> A C. ( B vH x ) ) ) ) )
67 66 an32s 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ x e. HAtoms ) -> ( x C_ A -> ( -. B C_ A -> ( A C. ( B vH C ) -> A C. ( B vH x ) ) ) ) )
68 67 com34 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ x e. HAtoms ) -> ( x C_ A -> ( A C. ( B vH C ) -> ( -. B C_ A -> A C. ( B vH x ) ) ) ) )
69 68 imp45 
 |-  ( ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ x e. HAtoms ) /\ ( x C_ A /\ ( A C. ( B vH C ) /\ -. B C_ A ) ) ) -> A C. ( B vH x ) )
70 simpr 
 |-  ( ( B e. CH /\ x e. CH ) -> x e. CH )
71 70 42 jca 
 |-  ( ( B e. CH /\ x e. CH ) -> ( x e. CH /\ ( B vH x ) e. CH ) )
72 9 7 71 syl2an 
 |-  ( ( B e. HAtoms /\ x e. HAtoms ) -> ( x e. CH /\ ( B vH x ) e. CH ) )
73 cvnbtwn3 
 |-  ( ( x e. CH /\ ( B vH x ) e. CH /\ A e. CH ) -> ( x  ( ( x C_ A /\ A C. ( B vH x ) ) -> A = x ) ) )
74 1 73 mp3an3 
 |-  ( ( x e. CH /\ ( B vH x ) e. CH ) -> ( x  ( ( x C_ A /\ A C. ( B vH x ) ) -> A = x ) ) )
75 74 exp4a 
 |-  ( ( x e. CH /\ ( B vH x ) e. CH ) -> ( x  ( x C_ A -> ( A C. ( B vH x ) -> A = x ) ) ) )
76 75 com23 
 |-  ( ( x e. CH /\ ( B vH x ) e. CH ) -> ( x C_ A -> ( x  ( A C. ( B vH x ) -> A = x ) ) ) )
77 76 imp4a 
 |-  ( ( x e. CH /\ ( B vH x ) e. CH ) -> ( x C_ A -> ( ( x  A = x ) ) )
78 72 77 syl 
 |-  ( ( B e. HAtoms /\ x e. HAtoms ) -> ( x C_ A -> ( ( x  A = x ) ) )
79 78 adantlr 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ x e. HAtoms ) -> ( x C_ A -> ( ( x  A = x ) ) )
80 79 imp 
 |-  ( ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ x e. HAtoms ) /\ x C_ A ) -> ( ( x  A = x ) )
81 80 adantrr 
 |-  ( ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ x e. HAtoms ) /\ ( x C_ A /\ ( A C. ( B vH C ) /\ -. B C_ A ) ) ) -> ( ( x  A = x ) )
82 18 69 81 mp2and 
 |-  ( ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ x e. HAtoms ) /\ ( x C_ A /\ ( A C. ( B vH C ) /\ -. B C_ A ) ) ) -> A = x )
83 82 eleq1d 
 |-  ( ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ x e. HAtoms ) /\ ( x C_ A /\ ( A C. ( B vH C ) /\ -. B C_ A ) ) ) -> ( A e. HAtoms <-> x e. HAtoms ) )
84 83 biimprcd 
 |-  ( x e. HAtoms -> ( ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ x e. HAtoms ) /\ ( x C_ A /\ ( A C. ( B vH C ) /\ -. B C_ A ) ) ) -> A e. HAtoms ) )
85 84 exp4c 
 |-  ( x e. HAtoms -> ( ( B e. HAtoms /\ C e. HAtoms ) -> ( x e. HAtoms -> ( ( x C_ A /\ ( A C. ( B vH C ) /\ -. B C_ A ) ) -> A e. HAtoms ) ) ) )
86 85 pm2.43b 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( x e. HAtoms -> ( ( x C_ A /\ ( A C. ( B vH C ) /\ -. B C_ A ) ) -> A e. HAtoms ) ) )
87 86 imp 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ x e. HAtoms ) -> ( ( x C_ A /\ ( A C. ( B vH C ) /\ -. B C_ A ) ) -> A e. HAtoms ) )
88 87 exp4d 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ x e. HAtoms ) -> ( x C_ A -> ( A C. ( B vH C ) -> ( -. B C_ A -> A e. HAtoms ) ) ) )
89 88 rexlimdva 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( E. x e. HAtoms x C_ A -> ( A C. ( B vH C ) -> ( -. B C_ A -> A e. HAtoms ) ) ) )
90 2 89 syl5 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( A =/= 0H -> ( A C. ( B vH C ) -> ( -. B C_ A -> A e. HAtoms ) ) ) )
91 90 imp32 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ ( A =/= 0H /\ A C. ( B vH C ) ) ) -> ( -. B C_ A -> A e. HAtoms ) )