Metamath Proof Explorer

Theorem atcvat2

Description: A Hilbert lattice element covered by the join of two distinct atoms is an atom. (Contributed by NM, 29-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion atcvat2 
|- ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) -> ( ( -. B = C /\ A  A e. HAtoms ) )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( A  if ( A e. CH , A , 0H )
2 1 anbi2d 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( ( -. B = C /\ A  ( -. B = C /\ if ( A e. CH , A , 0H )
3 eleq1 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( A e. HAtoms <-> if ( A e. CH , A , 0H ) e. HAtoms ) )
4 2 3 imbi12d 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( ( ( -. B = C /\ A  A e. HAtoms ) <-> ( ( -. B = C /\ if ( A e. CH , A , 0H )  if ( A e. CH , A , 0H ) e. HAtoms ) ) )
5 4 imbi2d 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( -. B = C /\ A  A e. HAtoms ) ) <-> ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( -. B = C /\ if ( A e. CH , A , 0H )  if ( A e. CH , A , 0H ) e. HAtoms ) ) ) )
6 h0elch 
 |-  0H e. CH
7 6 elimel 
 |-  if ( A e. CH , A , 0H ) e. CH
8 7 atcvat2i 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( -. B = C /\ if ( A e. CH , A , 0H )  if ( A e. CH , A , 0H ) e. HAtoms ) )
9 5 8 dedth 
 |-  ( A e. CH -> ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( -. B = C /\ A  A e. HAtoms ) ) )
10 9 3impib 
 |-  ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) -> ( ( -. B = C /\ A  A e. HAtoms ) )