# Metamath Proof Explorer

## Theorem lspid

Description: The span of a subspace is itself. ( spanid analog.) (Contributed by NM, 15-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lspid.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
lspid.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
Assertion lspid ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {N}\left({U}\right)={U}$

### Proof

Step Hyp Ref Expression
1 lspid.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
2 lspid.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
3 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
4 3 1 lssss ${⊢}{U}\in {S}\to {U}\subseteq {\mathrm{Base}}_{{W}}$
5 3 1 2 lspval ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\subseteq {\mathrm{Base}}_{{W}}\right)\to {N}\left({U}\right)=\bigcap \left\{{t}\in {S}|{U}\subseteq {t}\right\}$
6 4 5 sylan2 ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {N}\left({U}\right)=\bigcap \left\{{t}\in {S}|{U}\subseteq {t}\right\}$
7 intmin ${⊢}{U}\in {S}\to \bigcap \left\{{t}\in {S}|{U}\subseteq {t}\right\}={U}$
8 7 adantl ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to \bigcap \left\{{t}\in {S}|{U}\subseteq {t}\right\}={U}$
9 6 8 eqtrd ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {N}\left({U}\right)={U}$