Metamath Proof Explorer

Theorem h1datom

Description: A 1-dimensional subspace is an atom. (Contributed by NM, 22-Jul-2001) (New usage is discouraged.)

Ref Expression
Assertion h1datom 
|- ( ( A e. CH /\ B e. ~H ) -> ( A C_ ( _|_ ` ( _|_ ` { B } ) ) -> ( A = ( _|_ ` ( _|_ ` { B } ) ) \/ A = 0H ) ) )

Proof

Step Hyp Ref Expression
1 sseq1 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( A C_ ( _|_ ` ( _|_ ` { B } ) ) <-> if ( A e. CH , A , 0H ) C_ ( _|_ ` ( _|_ ` { B } ) ) ) )
2 eqeq1 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( A = ( _|_ ` ( _|_ ` { B } ) ) <-> if ( A e. CH , A , 0H ) = ( _|_ ` ( _|_ ` { B } ) ) ) )
3 eqeq1 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( A = 0H <-> if ( A e. CH , A , 0H ) = 0H ) )
4 2 3 orbi12d 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( ( A = ( _|_ ` ( _|_ ` { B } ) ) \/ A = 0H ) <-> ( if ( A e. CH , A , 0H ) = ( _|_ ` ( _|_ ` { B } ) ) \/ if ( A e. CH , A , 0H ) = 0H ) ) )
5 1 4 imbi12d 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( ( A C_ ( _|_ ` ( _|_ ` { B } ) ) -> ( A = ( _|_ ` ( _|_ ` { B } ) ) \/ A = 0H ) ) <-> ( if ( A e. CH , A , 0H ) C_ ( _|_ ` ( _|_ ` { B } ) ) -> ( if ( A e. CH , A , 0H ) = ( _|_ ` ( _|_ ` { B } ) ) \/ if ( A e. CH , A , 0H ) = 0H ) ) ) )
6 sneq 
 |-  ( B = if ( B e. ~H , B , 0h ) -> { B } = { if ( B e. ~H , B , 0h ) } )
7 6 fveq2d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( _|_ ` { B } ) = ( _|_ ` { if ( B e. ~H , B , 0h ) } ) )
8 7 fveq2d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( _|_ ` ( _|_ ` { B } ) ) = ( _|_ ` ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) )
9 8 sseq2d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( if ( A e. CH , A , 0H ) C_ ( _|_ ` ( _|_ ` { B } ) ) <-> if ( A e. CH , A , 0H ) C_ ( _|_ ` ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) ) )
10 8 eqeq2d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( if ( A e. CH , A , 0H ) = ( _|_ ` ( _|_ ` { B } ) ) <-> if ( A e. CH , A , 0H ) = ( _|_ ` ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) ) )
11 10 orbi1d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( if ( A e. CH , A , 0H ) = ( _|_ ` ( _|_ ` { B } ) ) \/ if ( A e. CH , A , 0H ) = 0H ) <-> ( if ( A e. CH , A , 0H ) = ( _|_ ` ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) \/ if ( A e. CH , A , 0H ) = 0H ) ) )
12 9 11 imbi12d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( if ( A e. CH , A , 0H ) C_ ( _|_ ` ( _|_ ` { B } ) ) -> ( if ( A e. CH , A , 0H ) = ( _|_ ` ( _|_ ` { B } ) ) \/ if ( A e. CH , A , 0H ) = 0H ) ) <-> ( if ( A e. CH , A , 0H ) C_ ( _|_ ` ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) -> ( if ( A e. CH , A , 0H ) = ( _|_ ` ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) \/ if ( A e. CH , A , 0H ) = 0H ) ) ) )
13 h0elch 
 |-  0H e. CH
14 13 elimel 
 |-  if ( A e. CH , A , 0H ) e. CH
15 ifhvhv0 
 |-  if ( B e. ~H , B , 0h ) e. ~H
16 14 15 h1datomi 
 |-  ( if ( A e. CH , A , 0H ) C_ ( _|_ ` ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) -> ( if ( A e. CH , A , 0H ) = ( _|_ ` ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) \/ if ( A e. CH , A , 0H ) = 0H ) )
17 5 12 16 dedth2h 
 |-  ( ( A e. CH /\ B e. ~H ) -> ( A C_ ( _|_ ` ( _|_ ` { B } ) ) -> ( A = ( _|_ ` ( _|_ ` { B } ) ) \/ A = 0H ) ) )