Theorem spansnss

Description: The span of the singleton of an element of a subspace is included in the subspace. (Contributed by NM, 5-Jun-2004) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		shel	|- ( ( A e. SH /\ B e. A ) -> B e. ~H )
2		elspansn	|- ( B e. ~H -> ( x e. ( span ` { B } ) <-> E. y e. CC x = ( y .h B ) ) )
3	1 2	syl	|- ( ( A e. SH /\ B e. A ) -> ( x e. ( span ` { B } ) <-> E. y e. CC x = ( y .h B ) ) )
4		shmulcl	|- ( ( A e. SH /\ y e. CC /\ B e. A ) -> ( y .h B ) e. A )
5		eleq1a	|- ( ( y .h B ) e. A -> ( x = ( y .h B ) -> x e. A ) )
6	4 5	syl	|- ( ( A e. SH /\ y e. CC /\ B e. A ) -> ( x = ( y .h B ) -> x e. A ) )
7	6	3exp	|- ( A e. SH -> ( y e. CC -> ( B e. A -> ( x = ( y .h B ) -> x e. A ) ) ) )
8	7	com23	|- ( A e. SH -> ( B e. A -> ( y e. CC -> ( x = ( y .h B ) -> x e. A ) ) ) )
9	8	imp	|- ( ( A e. SH /\ B e. A ) -> ( y e. CC -> ( x = ( y .h B ) -> x e. A ) ) )
10	9	rexlimdv	|- ( ( A e. SH /\ B e. A ) -> ( E. y e. CC x = ( y .h B ) -> x e. A ) )
11	3 10	sylbid	|- ( ( A e. SH /\ B e. A ) -> ( x e. ( span ` { B } ) -> x e. A ) )
12	11	ssrdv	|- ( ( A e. SH /\ B e. A ) -> ( span ` { B } ) C_ A )