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=\mathrm{AlgSpan}\left(W\right)$$
	aspval.v	$$⊢V={\mathrm{Base}}_W$$
Assertion	aspssid	$$⊢\left(W\in \mathrm{AssAlg}\wedge S\subseteq V\right)\to S\subseteq A\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		aspval.a	$$⊢A=\mathrm{AlgSpan}\left(W\right)$$
2		aspval.v	$$⊢V={\mathrm{Base}}_W$$
3		ssintub	$$⊢S\subseteq \bigcap \left\{t\in \left(\mathrm{SubRing}\left(W\right)\cap \mathrm{LSubSp}\left(W\right)\right)|S\subseteq t\right\}$$
4		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
5	1 2 4	aspval	$$⊢\left(W\in \mathrm{AssAlg}\wedge S\subseteq V\right)\to A\left(S\right)=\bigcap \left\{t\in \left(\mathrm{SubRing}\left(W\right)\cap \mathrm{LSubSp}\left(W\right)\right)|S\subseteq t\right\}$$
6	3 5	sseqtrrid	$$⊢\left(W\in \mathrm{AssAlg}\wedge S\subseteq V\right)\to S\subseteq A\left(S\right)$$