# Metamath Proof Explorer

## Theorem aspsubrg

Description: The algebraic span of a set of vectors is a subring of the algebra. (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 aspsubrg ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\right)\to {A}\left({S}\right)\in \mathrm{SubRing}\left({W}\right)$

### Proof

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