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 | ||
lspss.n | |||
Assertion | lspidm |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lspss.v | ||
2 | lspss.n | ||
3 | eqid | ||
4 | 1 3 2 | lspcl | |
5 | 3 2 | lspid | |
6 | 4 5 | syldan |