# Metamath Proof Explorer

## Theorem asplss

Description: The algebraic span of a set of vectors is a vector subspace. (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Hypotheses aspval.a ${⊢}{A}=\mathrm{AlgSpan}\left({W}\right)$
aspval.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
aspval.l ${⊢}{L}=\mathrm{LSubSp}\left({W}\right)$
Assertion asplss ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\right)\to {A}\left({S}\right)\in {L}$

### Proof

Step Hyp Ref Expression
1 aspval.a ${⊢}{A}=\mathrm{AlgSpan}\left({W}\right)$
2 aspval.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
3 aspval.l ${⊢}{L}=\mathrm{LSubSp}\left({W}\right)$
4 1 2 3 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 {L}\right)|{S}\subseteq {t}\right\}$
5 assalmod ${⊢}{W}\in \mathrm{AssAlg}\to {W}\in \mathrm{LMod}$
6 5 adantr ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\right)\to {W}\in \mathrm{LMod}$
7 ssrab2 ${⊢}\left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap {L}\right)|{S}\subseteq {t}\right\}\subseteq \mathrm{SubRing}\left({W}\right)\cap {L}$
8 inss2 ${⊢}\mathrm{SubRing}\left({W}\right)\cap {L}\subseteq {L}$
9 7 8 sstri ${⊢}\left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap {L}\right)|{S}\subseteq {t}\right\}\subseteq {L}$
10 9 a1i ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\right)\to \left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap {L}\right)|{S}\subseteq {t}\right\}\subseteq {L}$
11 fvex ${⊢}{A}\left({S}\right)\in \mathrm{V}$
12 4 11 eqeltrrdi ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\right)\to \bigcap \left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap {L}\right)|{S}\subseteq {t}\right\}\in \mathrm{V}$
13 intex ${⊢}\left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap {L}\right)|{S}\subseteq {t}\right\}\ne \varnothing ↔\bigcap \left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap {L}\right)|{S}\subseteq {t}\right\}\in \mathrm{V}$
14 12 13 sylibr ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\right)\to \left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap {L}\right)|{S}\subseteq {t}\right\}\ne \varnothing$
15 3 lssintcl ${⊢}\left({W}\in \mathrm{LMod}\wedge \left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap {L}\right)|{S}\subseteq {t}\right\}\subseteq {L}\wedge \left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap {L}\right)|{S}\subseteq {t}\right\}\ne \varnothing \right)\to \bigcap \left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap {L}\right)|{S}\subseteq {t}\right\}\in {L}$
16 6 10 14 15 syl3anc ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\right)\to \bigcap \left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap {L}\right)|{S}\subseteq {t}\right\}\in {L}$
17 4 16 eqeltrd ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\right)\to {A}\left({S}\right)\in {L}$