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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspval.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lspval.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion lspcl ( ( 𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑈 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 lspval.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspval.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 lspval.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 1 2 3 lspf ⊢ ( 𝑊 ∈ LMod → 𝑁 : 𝒫 𝑉 ⟶ 𝑆 )
5 1 fvexi ⊢ 𝑉 ∈ V
6 5 elpw2 ⊢ ( 𝑈 ∈ 𝒫 𝑉 ↔ 𝑈 ⊆ 𝑉 )
7 6 biimpri ⊢ ( 𝑈 ⊆ 𝑉 → 𝑈 ∈ 𝒫 𝑉 )
8 ffvelcdm ⊢ ( ( 𝑁 : 𝒫 𝑉 ⟶ 𝑆 ∧ 𝑈 ∈ 𝒫 𝑉 ) → ( 𝑁 ‘ 𝑈 ) ∈ 𝑆 )
9 4 7 8 syl2an ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑈 ) ∈ 𝑆 )