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 V = Base W
lspss.n N = LSpan W
Assertion lspidm W LMod U V N N U = N U

Proof

Step Hyp Ref Expression
1 lspss.v V = Base W
2 lspss.n N = LSpan W
3 eqid LSubSp W = LSubSp W
4 1 3 2 lspcl W LMod U V N U LSubSp W
5 3 2 lspid W LMod N U LSubSp W N N U = N U
6 4 5 syldan W LMod U V N N U = N U