This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrdi 
 |-  ( 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 )