Metamath Proof Explorer
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 |
|
ffvelrn |
⊢ ( ( 𝑁 : 𝒫 𝑉 ⟶ 𝑆 ∧ 𝑈 ∈ 𝒫 𝑉 ) → ( 𝑁 ‘ 𝑈 ) ∈ 𝑆 ) |
9 |
4 7 8
|
syl2an |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑈 ) ∈ 𝑆 ) |