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 = Base W
lspval.s S = LSubSp W
lspval.n N = LSpan W
Assertion lspcl W LMod U V N U S


Step Hyp Ref Expression
1 lspval.v V = Base W
2 lspval.s S = LSubSp W
3 lspval.n N = LSpan W
4 1 2 3 lspf W LMod N : 𝒫 V S
5 1 fvexi V V
6 5 elpw2 U 𝒫 V U V
7 6 biimpri U V U 𝒫 V
8 ffvelrn N : 𝒫 V S U 𝒫 V N U S
9 4 7 8 syl2an W LMod U V N U S