# Metamath Proof Explorer

## Theorem aspid

Description: The algebraic span of a subalgebra is itself. ( spanid 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}}$
aspval.l ${⊢}{L}=\mathrm{LSubSp}\left({W}\right)$
Assertion aspid ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\wedge {S}\in {L}\right)\to {A}\left({S}\right)={S}$

### 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 simp1 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\wedge {S}\in {L}\right)\to {W}\in \mathrm{AssAlg}$
5 2 subrgss ${⊢}{S}\in \mathrm{SubRing}\left({W}\right)\to {S}\subseteq {V}$
6 5 3ad2ant2 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\wedge {S}\in {L}\right)\to {S}\subseteq {V}$
7 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\}$
8 4 6 7 syl2anc ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\wedge {S}\in {L}\right)\to {A}\left({S}\right)=\bigcap \left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap {L}\right)|{S}\subseteq {t}\right\}$
9 3simpc ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\wedge {S}\in {L}\right)\to \left({S}\in \mathrm{SubRing}\left({W}\right)\wedge {S}\in {L}\right)$
10 elin ${⊢}{S}\in \left(\mathrm{SubRing}\left({W}\right)\cap {L}\right)↔\left({S}\in \mathrm{SubRing}\left({W}\right)\wedge {S}\in {L}\right)$
11 9 10 sylibr ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\wedge {S}\in {L}\right)\to {S}\in \left(\mathrm{SubRing}\left({W}\right)\cap {L}\right)$
12 intmin ${⊢}{S}\in \left(\mathrm{SubRing}\left({W}\right)\cap {L}\right)\to \bigcap \left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap {L}\right)|{S}\subseteq {t}\right\}={S}$
13 11 12 syl ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\wedge {S}\in {L}\right)\to \bigcap \left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap {L}\right)|{S}\subseteq {t}\right\}={S}$
14 8 13 eqtrd ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\in \mathrm{SubRing}\left({W}\right)\wedge {S}\in {L}\right)\to {A}\left({S}\right)={S}$