Description: Two ways to express that vectors have different spans. (Contributed by NM, 28-May-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lspsnne1.v | |
|
lspsnne1.o | |
||
lspsnne1.n | |
||
lspsnne1.w | |
||
lspsnne1.x | |
||
lspsnne1.y | |
||
lspsnne1.e | |
||
Assertion | lspsnne1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lspsnne1.v | |
|
2 | lspsnne1.o | |
|
3 | lspsnne1.n | |
|
4 | lspsnne1.w | |
|
5 | lspsnne1.x | |
|
6 | lspsnne1.y | |
|
7 | lspsnne1.e | |
|
8 | eqid | |
|
9 | lveclmod | |
|
10 | 4 9 | syl | |
11 | 1 8 3 | lspsncl | |
12 | 10 6 11 | syl2anc | |
13 | 5 | eldifad | |
14 | 1 8 3 10 12 13 | lspsnel5 | |
15 | 14 | notbid | |
16 | 1 2 3 4 5 6 | lspsncmp | |
17 | 16 | necon3bbid | |
18 | 15 17 | bitrd | |
19 | 7 18 | mpbird | |