This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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 ffvelcdm ⊢ N : 𝒫 V ⟶ S ∧ U ∈ 𝒫 V → N ⁡ U ∈ S
9 4 7 8 syl2an ⊢ W ∈ LMod ∧ U ⊆ V → N ⁡ U ∈ S