Metamath Proof Explorer

Theorem h1da

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

Ref Expression
Assertion h1da 
|- ( ( A e. ~H /\ A =/= 0h ) -> ( _|_ ` ( _|_ ` { A } ) ) e. HAtoms )

Proof

Step Hyp Ref Expression
1 snssi 
 |-  ( A e. ~H -> { A } C_ ~H )
2 occl 
 |-  ( { A } C_ ~H -> ( _|_ ` { A } ) e. CH )
3 choccl 
 |-  ( ( _|_ ` { A } ) e. CH -> ( _|_ ` ( _|_ ` { A } ) ) e. CH )
4 1 2 3 3syl 
 |-  ( A e. ~H -> ( _|_ ` ( _|_ ` { A } ) ) e. CH )
5 4 adantr 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( _|_ ` ( _|_ ` { A } ) ) e. CH )
6 h1dn0 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( _|_ ` ( _|_ ` { A } ) ) =/= 0H )
7 h1datom 
 |-  ( ( x e. CH /\ A e. ~H ) -> ( x C_ ( _|_ ` ( _|_ ` { A } ) ) -> ( x = ( _|_ ` ( _|_ ` { A } ) ) \/ x = 0H ) ) )
8 7 expcom 
 |-  ( A e. ~H -> ( x e. CH -> ( x C_ ( _|_ ` ( _|_ ` { A } ) ) -> ( x = ( _|_ ` ( _|_ ` { A } ) ) \/ x = 0H ) ) ) )
9 8 ralrimiv 
 |-  ( A e. ~H -> A. x e. CH ( x C_ ( _|_ ` ( _|_ ` { A } ) ) -> ( x = ( _|_ ` ( _|_ ` { A } ) ) \/ x = 0H ) ) )
10 9 adantr 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> A. x e. CH ( x C_ ( _|_ ` ( _|_ ` { A } ) ) -> ( x = ( _|_ ` ( _|_ ` { A } ) ) \/ x = 0H ) ) )
11 6 10 jca 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( ( _|_ ` ( _|_ ` { A } ) ) =/= 0H /\ A. x e. CH ( x C_ ( _|_ ` ( _|_ ` { A } ) ) -> ( x = ( _|_ ` ( _|_ ` { A } ) ) \/ x = 0H ) ) ) )
12 elat2 
 |-  ( ( _|_ ` ( _|_ ` { A } ) ) e. HAtoms <-> ( ( _|_ ` ( _|_ ` { A } ) ) e. CH /\ ( ( _|_ ` ( _|_ ` { A } ) ) =/= 0H /\ A. x e. CH ( x C_ ( _|_ ` ( _|_ ` { A } ) ) -> ( x = ( _|_ ` ( _|_ ` { A } ) ) \/ x = 0H ) ) ) ) )
13 5 11 12 sylanbrc 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( _|_ ` ( _|_ ` { A } ) ) e. HAtoms )