Theorem lspssid

Description: A set of vectors is a subset of its span. ( spanss2 analog.) (Contributed by NM, 6-Feb-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lspss.v	|- V = ( Base ` W )
	lspss.n	|- N = ( LSpan ` W )
Assertion	lspssid	|- ( ( W e. LMod /\ U C_ V ) -> U C_ ( N ` U ) )

Proof

Step	Hyp	Ref	Expression
1		lspss.v	|- V = ( Base ` W )
2		lspss.n	|- N = ( LSpan ` W )
3		ssintub	|- U C_ |^| { t e. ( LSubSp ` W ) | U C_ t }
4		eqid	|- ( LSubSp ` W ) = ( LSubSp ` W )
5	1 4 2	lspval	|- ( ( W e. LMod /\ U C_ V ) -> ( N ` U ) = |^| { t e. ( LSubSp ` W ) | U C_ t } )
6	3 5	sseqtrrid	|- ( ( W e. LMod /\ U C_ V ) -> U C_ ( N ` U ) )