# Metamath Proof Explorer

## Theorem aspss

Description: Span preserves subset ordering. ( spanss 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 aspss ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\wedge {T}\subseteq {S}\right)\to {A}\left({T}\right)\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 simpl3 ${⊢}\left(\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\wedge {T}\subseteq {S}\right)\wedge {t}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)\right)\to {T}\subseteq {S}$
4 sstr2 ${⊢}{T}\subseteq {S}\to \left({S}\subseteq {t}\to {T}\subseteq {t}\right)$
5 3 4 syl ${⊢}\left(\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\wedge {T}\subseteq {S}\right)\wedge {t}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)\right)\to \left({S}\subseteq {t}\to {T}\subseteq {t}\right)$
6 5 ss2rabdv ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\wedge {T}\subseteq {S}\right)\to \left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)|{S}\subseteq {t}\right\}\subseteq \left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)|{T}\subseteq {t}\right\}$
7 intss ${⊢}\left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)|{S}\subseteq {t}\right\}\subseteq \left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)|{T}\subseteq {t}\right\}\to \bigcap \left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)|{T}\subseteq {t}\right\}\subseteq \bigcap \left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)|{S}\subseteq {t}\right\}$
8 6 7 syl ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\wedge {T}\subseteq {S}\right)\to \bigcap \left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)|{T}\subseteq {t}\right\}\subseteq \bigcap \left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)|{S}\subseteq {t}\right\}$
9 simp1 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\wedge {T}\subseteq {S}\right)\to {W}\in \mathrm{AssAlg}$
10 simp3 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\wedge {T}\subseteq {S}\right)\to {T}\subseteq {S}$
11 simp2 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\wedge {T}\subseteq {S}\right)\to {S}\subseteq {V}$
12 10 11 sstrd ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\wedge {T}\subseteq {S}\right)\to {T}\subseteq {V}$
13 eqid ${⊢}\mathrm{LSubSp}\left({W}\right)=\mathrm{LSubSp}\left({W}\right)$
14 1 2 13 aspval ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {T}\subseteq {V}\right)\to {A}\left({T}\right)=\bigcap \left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)|{T}\subseteq {t}\right\}$
15 9 12 14 syl2anc ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\wedge {T}\subseteq {S}\right)\to {A}\left({T}\right)=\bigcap \left\{{t}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)|{T}\subseteq {t}\right\}$
16 1 2 13 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\}$
17 16 3adant3 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\wedge {T}\subseteq {S}\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\}$
18 8 15 17 3sstr4d ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\wedge {T}\subseteq {S}\right)\to {A}\left({T}\right)\subseteq {A}\left({S}\right)$