Theorem lspsnss

Description: The span of the singleton of a subspace member is included in the subspace. ( spansnss analog.) (Contributed by NM, 9-Apr-2014) (Revised by Mario Carneiro, 4-Sep-2014)

	Ref	Expression
Hypotheses	lspsnss.s	|- S = ( LSubSp ` W )
	lspsnss.n	|- N = ( LSpan ` W )
Assertion	lspsnss	|- ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( N ` { X } ) C_ U )

Proof

Step	Hyp	Ref	Expression
1		lspsnss.s	|- S = ( LSubSp ` W )
2		lspsnss.n	|- N = ( LSpan ` W )
3		snssi	|- ( X e. U -> { X } C_ U )
4	1 2	lspssp	|- ( ( W e. LMod /\ U e. S /\ { X } C_ U ) -> ( N ` { X } ) C_ U )
5	3 4	syl3an3	|- ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( N ` { X } ) C_ U )