Metamath Proof Explorer


Theorem dochfln0

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 H=LHypK
dochfln0.o ˙=ocHKW
dochfln0.u U=DVecHKW
dochfln0.v V=BaseU
dochfln0.r R=ScalarU
dochfln0.n N=0R
dochfln0.z 0˙=0U
dochfln0.f F=LFnlU
dochfln0.l L=LKerU
dochfln0.k φKHLWH
dochfln0.g φGF
dochfln0.x φX˙LG0˙
Assertion dochfln0 φGXN

Proof

Step Hyp Ref Expression
1 dochfln0.h H=LHypK
2 dochfln0.o ˙=ocHKW
3 dochfln0.u U=DVecHKW
4 dochfln0.v V=BaseU
5 dochfln0.r R=ScalarU
6 dochfln0.n N=0R
7 dochfln0.z 0˙=0U
8 dochfln0.f F=LFnlU
9 dochfln0.l L=LKerU
10 dochfln0.k φKHLWH
11 dochfln0.g φGF
12 dochfln0.x φX˙LG0˙
13 1 3 10 dvhlmod φULMod
14 4 8 9 13 11 lkrssv φLGV
15 1 3 4 2 dochssv KHLWHLGV˙LGV
16 10 14 15 syl2anc φ˙LGV
17 16 ssdifd φ˙LG0˙V0˙
18 17 12 sseldd φXV0˙
19 1 2 3 4 7 10 18 dochnel φ¬X˙X
20 12 eldifad φX˙LG
21 16 20 sseldd φXV
22 21 biantrurd φGX=NXVGX=N
23 4 5 6 8 9 ellkr ULModGFXLGXVGX=N
24 13 11 23 syl2anc φXLGXVGX=N
25 1 2 3 4 7 8 9 10 11 12 dochsnkr φLG=˙X
26 25 eleq2d φXLGX˙X
27 22 24 26 3bitr2rd φX˙XGX=N
28 27 necon3bbid φ¬X˙XGXN
29 19 28 mpbid φGXN