Theorem sh1dle

Description: A 1-dimensional subspace is less than or equal to any subspace containing its generating vector. (Contributed by NM, 24-Nov-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	sh1dle	|- ( ( A e. SH /\ B e. A ) -> ( _|_ ` ( _|_ ` { B } ) ) C_ A )

Proof

Step	Hyp	Ref	Expression
1		shel	|- ( ( A e. SH /\ B e. A ) -> B e. ~H )
2		spansn	|- ( B e. ~H -> ( span ` { B } ) = ( _|_ ` ( _|_ ` { B } ) ) )
3	1 2	syl	|- ( ( A e. SH /\ B e. A ) -> ( span ` { B } ) = ( _|_ ` ( _|_ ` { B } ) ) )
4		spansnss	|- ( ( A e. SH /\ B e. A ) -> ( span ` { B } ) C_ A )
5	3 4	eqsstrrd	|- ( ( A e. SH /\ B e. A ) -> ( _|_ ` ( _|_ ` { B } ) ) C_ A )