Description: The span of a set of vectors is idempotent. (Contributed by NM, 22-Feb-2014) (Revised by Mario Carneiro, 19-Jun-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lspss.v | ⊢ 𝑉 = ( Base ‘ 𝑊 ) | |
lspss.n | ⊢ 𝑁 = ( LSpan ‘ 𝑊 ) | ||
Assertion | lspidm | ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑈 ) ) = ( 𝑁 ‘ 𝑈 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lspss.v | ⊢ 𝑉 = ( Base ‘ 𝑊 ) | |
2 | lspss.n | ⊢ 𝑁 = ( LSpan ‘ 𝑊 ) | |
3 | eqid | ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 ) | |
4 | 1 3 2 | lspcl | ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑈 ) ∈ ( LSubSp ‘ 𝑊 ) ) |
5 | 3 2 | lspid | ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ 𝑈 ) ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑈 ) ) = ( 𝑁 ‘ 𝑈 ) ) |
6 | 4 5 | syldan | ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑈 ) ) = ( 𝑁 ‘ 𝑈 ) ) |