This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( LHyp ` K )
dochfln0.o 
|- ._|_ = ( ( ocH ` K ) ` W )
dochfln0.u 
|- U = ( ( DVecH ` K ) ` W )
dochfln0.v 
|- V = ( Base ` U )
dochfln0.r 
|- R = ( Scalar ` U )
dochfln0.n 
|- N = ( 0g ` R )
dochfln0.z 
|- .0. = ( 0g ` U )
dochfln0.f 
|- F = ( LFnl ` U )
dochfln0.l 
|- L = ( LKer ` U )
dochfln0.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dochfln0.g 
|- ( ph -> G e. F )
dochfln0.x 
|- ( ph -> X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )
Assertion dochfln0 
|- ( ph -> ( G ` X ) =/= N )

Proof

Step Hyp Ref Expression
1 dochfln0.h 
 |-  H = ( LHyp ` K )
2 dochfln0.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 dochfln0.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 dochfln0.v 
 |-  V = ( Base ` U )
5 dochfln0.r 
 |-  R = ( Scalar ` U )
6 dochfln0.n 
 |-  N = ( 0g ` R )
7 dochfln0.z 
 |-  .0. = ( 0g ` U )
8 dochfln0.f 
 |-  F = ( LFnl ` U )
9 dochfln0.l 
 |-  L = ( LKer ` U )
10 dochfln0.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
11 dochfln0.g 
 |-  ( ph -> G e. F )
12 dochfln0.x 
 |-  ( ph -> X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )
13 1 3 10 dvhlmod 
 |-  ( ph -> U e. LMod )
14 4 8 9 13 11 lkrssv 
 |-  ( ph -> ( L ` G ) C_ V )
15 1 3 4 2 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( L ` G ) C_ V ) -> ( ._|_ ` ( L ` G ) ) C_ V )
16 10 14 15 syl2anc 
 |-  ( ph -> ( ._|_ ` ( L ` G ) ) C_ V )
17 16 ssdifd 
 |-  ( ph -> ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) C_ ( V \ { .0. } ) )
18 17 12 sseldd 
 |-  ( ph -> X e. ( V \ { .0. } ) )
19 1 2 3 4 7 10 18 dochnel 
 |-  ( ph -> -. X e. ( ._|_ ` { X } ) )
20 12 eldifad 
 |-  ( ph -> X e. ( ._|_ ` ( L ` G ) ) )
21 16 20 sseldd 
 |-  ( ph -> X e. V )
22 21 biantrurd 
 |-  ( ph -> ( ( G ` X ) = N <-> ( X e. V /\ ( G ` X ) = N ) ) )
23 4 5 6 8 9 ellkr 
 |-  ( ( U e. LMod /\ G e. F ) -> ( X e. ( L ` G ) <-> ( X e. V /\ ( G ` X ) = N ) ) )
24 13 11 23 syl2anc 
 |-  ( ph -> ( X e. ( L ` G ) <-> ( X e. V /\ ( G ` X ) = N ) ) )
25 1 2 3 4 7 8 9 10 11 12 dochsnkr 
 |-  ( ph -> ( L ` G ) = ( ._|_ ` { X } ) )
26 25 eleq2d 
 |-  ( ph -> ( X e. ( L ` G ) <-> X e. ( ._|_ ` { X } ) ) )
27 22 24 26 3bitr2rd 
 |-  ( ph -> ( X e. ( ._|_ ` { X } ) <-> ( G ` X ) = N ) )
28 27 necon3bbid 
 |-  ( ph -> ( -. X e. ( ._|_ ` { X } ) <-> ( G ` X ) =/= N ) )
29 19 28 mpbid 
 |-  ( ph -> ( G ` X ) =/= N )