Metamath Proof Explorer


Theorem lspidm

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 ∧ 𝑈𝑉 ) → ( 𝑁 ‘ ( 𝑁𝑈 ) ) = ( 𝑁𝑈 ) )

Proof

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 ∧ 𝑈𝑉 ) → ( 𝑁 ‘ ( 𝑁𝑈 ) ) = ( 𝑁𝑈 ) )