Theorem aspssid

Description: A set of vectors is a subset of its span. ( spanss2 analog.) (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Hypotheses	aspval.a	|- A = ( AlgSpan ` W )
	aspval.v	|- V = ( Base ` W )
Assertion	aspssid	|- ( ( W e. AssAlg /\ S C_ V ) -> S C_ ( A ` S ) )

Proof

Step	Hyp	Ref	Expression
1		aspval.a	|- A = ( AlgSpan ` W )
2		aspval.v	|- V = ( Base ` W )
3		ssintub	|- S C_ |^| { t e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) | S C_ t }
4		eqid	|- ( LSubSp ` W ) = ( LSubSp ` W )
5	1 2 4	aspval	|- ( ( W e. AssAlg /\ S C_ V ) -> ( A ` S ) = |^| { t e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) | S C_ t } )
6	3 5	sseqtrrid	|- ( ( W e. AssAlg /\ S C_ V ) -> S C_ ( A ` S ) )