Description: A vector expressed as a sum belongs to the span of its components. (Contributed by NM, 9-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lsppreli.v | |
|
lsppreli.p | |
||
lsppreli.t | |
||
lsppreli.f | |
||
lsppreli.k | |
||
lsppreli.n | |
||
lsppreli.w | |
||
lsppreli.a | |
||
lsppreli.b | |
||
lsppreli.x | |
||
lsppreli.y | |
||
Assertion | lsppreli | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lsppreli.v | |
|
2 | lsppreli.p | |
|
3 | lsppreli.t | |
|
4 | lsppreli.f | |
|
5 | lsppreli.k | |
|
6 | lsppreli.n | |
|
7 | lsppreli.w | |
|
8 | lsppreli.a | |
|
9 | lsppreli.b | |
|
10 | lsppreli.x | |
|
11 | lsppreli.y | |
|
12 | 1 6 | lspsnsubg | |
13 | 7 10 12 | syl2anc | |
14 | 1 6 | lspsnsubg | |
15 | 7 11 14 | syl2anc | |
16 | 1 3 4 5 6 7 8 10 | lspsneli | |
17 | 1 3 4 5 6 7 9 11 | lspsneli | |
18 | eqid | |
|
19 | 2 18 | lsmelvali | |
20 | 13 15 16 17 19 | syl22anc | |
21 | 1 6 18 7 10 11 | lsmpr | |
22 | 20 21 | eleqtrrd | |