Metamath Proof Explorer


Theorem h1dn0

Description: A nonzero vector generates a (nonzero) 1-dimensional subspace. (Contributed by NM, 22-Jul-2001) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 h1did
 |-  ( A e. ~H -> A e. ( _|_ ` ( _|_ ` { A } ) ) )
2 eleq2
 |-  ( ( _|_ ` ( _|_ ` { A } ) ) = 0H -> ( A e. ( _|_ ` ( _|_ ` { A } ) ) <-> A e. 0H ) )
3 1 2 syl5ibcom
 |-  ( A e. ~H -> ( ( _|_ ` ( _|_ ` { A } ) ) = 0H -> A e. 0H ) )
4 elch0
 |-  ( A e. 0H <-> A = 0h )
5 3 4 syl6ib
 |-  ( A e. ~H -> ( ( _|_ ` ( _|_ ` { A } ) ) = 0H -> A = 0h ) )
6 5 necon3d
 |-  ( A e. ~H -> ( A =/= 0h -> ( _|_ ` ( _|_ ` { A } ) ) =/= 0H ) )
7 6 imp
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( _|_ ` ( _|_ ` { A } ) ) =/= 0H )