Description: The value of a functional is nonzero at a nonzero vector in the orthocomplement of its kernel. (Contributed by NM, 2-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dochfln0.h | |
|
dochfln0.o | |
||
dochfln0.u | |
||
dochfln0.v | |
||
dochfln0.r | |
||
dochfln0.n | |
||
dochfln0.z | |
||
dochfln0.f | |
||
dochfln0.l | |
||
dochfln0.k | |
||
dochfln0.g | |
||
dochfln0.x | |
||
Assertion | dochfln0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dochfln0.h | |
|
2 | dochfln0.o | |
|
3 | dochfln0.u | |
|
4 | dochfln0.v | |
|
5 | dochfln0.r | |
|
6 | dochfln0.n | |
|
7 | dochfln0.z | |
|
8 | dochfln0.f | |
|
9 | dochfln0.l | |
|
10 | dochfln0.k | |
|
11 | dochfln0.g | |
|
12 | dochfln0.x | |
|
13 | 1 3 10 | dvhlmod | |
14 | 4 8 9 13 11 | lkrssv | |
15 | 1 3 4 2 | dochssv | |
16 | 10 14 15 | syl2anc | |
17 | 16 | ssdifd | |
18 | 17 12 | sseldd | |
19 | 1 2 3 4 7 10 18 | dochnel | |
20 | 12 | eldifad | |
21 | 16 20 | sseldd | |
22 | 21 | biantrurd | |
23 | 4 5 6 8 9 | ellkr | |
24 | 13 11 23 | syl2anc | |
25 | 1 2 3 4 7 8 9 10 11 12 | dochsnkr | |
26 | 25 | eleq2d | |
27 | 22 24 26 | 3bitr2rd | |
28 | 27 | necon3bbid | |
29 | 19 28 | mpbid | |