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 )