Metamath Proof Explorer

Theorem atcvati

Description: A nonzero Hilbert lattice element less than the join of two atoms is an atom. (Contributed by NM, 28-Jun-2004) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 atoml.1 
 |-  A e. CH
2 1 atcvatlem 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ ( A =/= 0H /\ A C. ( B vH C ) ) ) -> ( -. B C_ A -> A e. HAtoms ) )
3 atelch 
 |-  ( C e. HAtoms -> C e. CH )
4 atelch 
 |-  ( B e. HAtoms -> B e. CH )
5 chjcom 
 |-  ( ( C e. CH /\ B e. CH ) -> ( C vH B ) = ( B vH C ) )
6 3 4 5 syl2an 
 |-  ( ( C e. HAtoms /\ B e. HAtoms ) -> ( C vH B ) = ( B vH C ) )
7 6 psseq2d 
 |-  ( ( C e. HAtoms /\ B e. HAtoms ) -> ( A C. ( C vH B ) <-> A C. ( B vH C ) ) )
8 7 anbi2d 
 |-  ( ( C e. HAtoms /\ B e. HAtoms ) -> ( ( A =/= 0H /\ A C. ( C vH B ) ) <-> ( A =/= 0H /\ A C. ( B vH C ) ) ) )
9 1 atcvatlem 
 |-  ( ( ( C e. HAtoms /\ B e. HAtoms ) /\ ( A =/= 0H /\ A C. ( C vH B ) ) ) -> ( -. C C_ A -> A e. HAtoms ) )
10 9 ex 
 |-  ( ( C e. HAtoms /\ B e. HAtoms ) -> ( ( A =/= 0H /\ A C. ( C vH B ) ) -> ( -. C C_ A -> A e. HAtoms ) ) )
11 8 10 sylbird 
 |-  ( ( C e. HAtoms /\ B e. HAtoms ) -> ( ( A =/= 0H /\ A C. ( B vH C ) ) -> ( -. C C_ A -> A e. HAtoms ) ) )
12 11 ancoms 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( A =/= 0H /\ A C. ( B vH C ) ) -> ( -. C C_ A -> A e. HAtoms ) ) )
13 12 imp 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ ( A =/= 0H /\ A C. ( B vH C ) ) ) -> ( -. C C_ A -> A e. HAtoms ) )
14 chlub 
 |-  ( ( B e. CH /\ C e. CH /\ A e. CH ) -> ( ( B C_ A /\ C C_ A ) <-> ( B vH C ) C_ A ) )
15 14 3comr 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( B C_ A /\ C C_ A ) <-> ( B vH C ) C_ A ) )
16 ssnpss 
 |-  ( ( B vH C ) C_ A -> -. A C. ( B vH C ) )
17 15 16 biimtrdi 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( B C_ A /\ C C_ A ) -> -. A C. ( B vH C ) ) )
18 17 con2d 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A C. ( B vH C ) -> -. ( B C_ A /\ C C_ A ) ) )
19 ianor 
 |-  ( -. ( B C_ A /\ C C_ A ) <-> ( -. B C_ A \/ -. C C_ A ) )
20 18 19 imbitrdi 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A C. ( B vH C ) -> ( -. B C_ A \/ -. C C_ A ) ) )
21 1 20 mp3an1 
 |-  ( ( B e. CH /\ C e. CH ) -> ( A C. ( B vH C ) -> ( -. B C_ A \/ -. C C_ A ) ) )
22 4 3 21 syl2an 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( A C. ( B vH C ) -> ( -. B C_ A \/ -. C C_ A ) ) )
23 22 imp 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ A C. ( B vH C ) ) -> ( -. B C_ A \/ -. C C_ A ) )
24 23 adantrl 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ ( A =/= 0H /\ A C. ( B vH C ) ) ) -> ( -. B C_ A \/ -. C C_ A ) )
25 2 13 24 mpjaod 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ ( A =/= 0H /\ A C. ( B vH C ) ) ) -> A e. HAtoms )
26 25 ex 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( A =/= 0H /\ A C. ( B vH C ) ) -> A e. HAtoms ) )