# Metamath Proof Explorer

## 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)$