# Metamath Proof Explorer

## Theorem lspcl

Description: The span of a set of vectors is a subspace. ( spancl analog.) (Contributed by NM, 9-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lspval.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
lspval.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
lspval.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
Assertion lspcl ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\subseteq {V}\right)\to {N}\left({U}\right)\in {S}$

### Proof

Step Hyp Ref Expression
1 lspval.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 lspval.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
3 lspval.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
4 1 2 3 lspf ${⊢}{W}\in \mathrm{LMod}\to {N}:𝒫{V}⟶{S}$
5 1 fvexi ${⊢}{V}\in \mathrm{V}$
6 5 elpw2 ${⊢}{U}\in 𝒫{V}↔{U}\subseteq {V}$
7 6 biimpri ${⊢}{U}\subseteq {V}\to {U}\in 𝒫{V}$
8 ffvelrn ${⊢}\left({N}:𝒫{V}⟶{S}\wedge {U}\in 𝒫{V}\right)\to {N}\left({U}\right)\in {S}$
9 4 7 8 syl2an ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\subseteq {V}\right)\to {N}\left({U}\right)\in {S}$