Description: The span of a pair of vectors equals the sum of the spans of their singletons. (Contributed by NM, 13-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lsmpr.v | |
|
lsmpr.n | |
||
lsmpr.p | |
||
lsmpr.w | |
||
lsmpr.x | |
||
lsmpr.y | |
||
Assertion | lsmpr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lsmpr.v | |
|
2 | lsmpr.n | |
|
3 | lsmpr.p | |
|
4 | lsmpr.w | |
|
5 | lsmpr.x | |
|
6 | lsmpr.y | |
|
7 | 5 | snssd | |
8 | 6 | snssd | |
9 | 1 2 | lspun | |
10 | 4 7 8 9 | syl3anc | |
11 | df-pr | |
|
12 | 11 | fveq2i | |
13 | 12 | a1i | |
14 | eqid | |
|
15 | 1 14 2 | lspsncl | |
16 | 4 5 15 | syl2anc | |
17 | 1 14 2 | lspsncl | |
18 | 4 6 17 | syl2anc | |
19 | 14 2 3 | lsmsp | |
20 | 4 16 18 19 | syl3anc | |
21 | 10 13 20 | 3eqtr4d | |