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 )