Metamath Proof Explorer

Theorem atord

Description: An ordering law for a Hilbert lattice atom and a commuting subspace. (Contributed by NM, 12-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion atord 
|- ( ( A e. CH /\ B e. HAtoms /\ A C_H B ) -> ( B C_ A \/ B C_ ( _|_ ` A ) ) )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( A C_H B <-> if ( A e. CH , A , 0H ) C_H B ) )
2 1 anbi2d 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( ( B e. HAtoms /\ A C_H B ) <-> ( B e. HAtoms /\ if ( A e. CH , A , 0H ) C_H B ) ) )
3 sseq2 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( B C_ A <-> B C_ if ( A e. CH , A , 0H ) ) )
4 fveq2 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( _|_ ` A ) = ( _|_ ` if ( A e. CH , A , 0H ) ) )
5 4 sseq2d 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( B C_ ( _|_ ` A ) <-> B C_ ( _|_ ` if ( A e. CH , A , 0H ) ) ) )
6 3 5 orbi12d 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( ( B C_ A \/ B C_ ( _|_ ` A ) ) <-> ( B C_ if ( A e. CH , A , 0H ) \/ B C_ ( _|_ ` if ( A e. CH , A , 0H ) ) ) ) )
7 2 6 imbi12d 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( ( ( B e. HAtoms /\ A C_H B ) -> ( B C_ A \/ B C_ ( _|_ ` A ) ) ) <-> ( ( B e. HAtoms /\ if ( A e. CH , A , 0H ) C_H B ) -> ( B C_ if ( A e. CH , A , 0H ) \/ B C_ ( _|_ ` if ( A e. CH , A , 0H ) ) ) ) ) )
8 h0elch 
 |-  0H e. CH
9 8 elimel 
 |-  if ( A e. CH , A , 0H ) e. CH
10 9 atordi 
 |-  ( ( B e. HAtoms /\ if ( A e. CH , A , 0H ) C_H B ) -> ( B C_ if ( A e. CH , A , 0H ) \/ B C_ ( _|_ ` if ( A e. CH , A , 0H ) ) ) )
11 7 10 dedth 
 |-  ( A e. CH -> ( ( B e. HAtoms /\ A C_H B ) -> ( B C_ A \/ B C_ ( _|_ ` A ) ) ) )
12 11 3impib 
 |-  ( ( A e. CH /\ B e. HAtoms /\ A C_H B ) -> ( B C_ A \/ B C_ ( _|_ ` A ) ) )