Description: Colinear functionals have equal kernels. (Contributed by NM, 28-Mar-2015) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lcdlkreq2.h | |
|
lcdlkreq2.u | |
||
lcdlkreq2.s | |
||
lcdlkreq2.r | |
||
lcdlkreq2.o | |
||
lcdlkreq2.l | |
||
lcdlkreq2.c | |
||
lcdlkreq2.v | |
||
lcdlkreq2.t | |
||
lcdlkreq2.k | |
||
lcdlkreq2.a | |
||
lcdlkreq2.i | |
||
lcdlkreq2.g | |
||
Assertion | lcdlkreq2N | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lcdlkreq2.h | |
|
2 | lcdlkreq2.u | |
|
3 | lcdlkreq2.s | |
|
4 | lcdlkreq2.r | |
|
5 | lcdlkreq2.o | |
|
6 | lcdlkreq2.l | |
|
7 | lcdlkreq2.c | |
|
8 | lcdlkreq2.v | |
|
9 | lcdlkreq2.t | |
|
10 | lcdlkreq2.k | |
|
11 | lcdlkreq2.a | |
|
12 | lcdlkreq2.i | |
|
13 | lcdlkreq2.g | |
|
14 | eqid | |
|
15 | eqid | |
|
16 | eqid | |
|
17 | 1 2 10 | dvhlvec | |
18 | 1 7 8 2 14 10 12 | lcdvbaselfl | |
19 | 1 2 15 16 7 9 10 | lcdvs | |
20 | 19 | oveqd | |
21 | 13 20 | eqtrd | |
22 | 3 4 5 14 6 15 16 17 11 18 21 | lkreqN | |