Metamath Proof Explorer

Theorem dochkr1

Description: A nonzero functional has a value of 1 at some argument belonging to the orthocomplement of its kernel (when its kernel is a closed hyperplane). Tighter version of lfl1 . (Contributed by NM, 2-Jan-2015)

Ref Expression
Hypotheses dochkr1.h 
|- H = ( LHyp ` K )
dochkr1.o 
|- ._|_ = ( ( ocH ` K ) ` W )
dochkr1.u 
|- U = ( ( DVecH ` K ) ` W )
dochkr1.v 
|- V = ( Base ` U )
dochkr1.r 
|- R = ( Scalar ` U )
dochkr1.z 
|- .0. = ( 0g ` U )
dochkr1.i 
|- .1. = ( 1r ` R )
dochkr1.f 
|- F = ( LFnl ` U )
dochkr1.l 
|- L = ( LKer ` U )
dochkr1.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dochkr1.g 
|- ( ph -> G e. F )
dochkr1.n 
|- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V )
Assertion dochkr1 
|- ( ph -> E. x e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) ( G ` x ) = .1. )

Proof

Step Hyp Ref Expression
1 dochkr1.h 
 |-  H = ( LHyp ` K )
2 dochkr1.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 dochkr1.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 dochkr1.v 
 |-  V = ( Base ` U )
5 dochkr1.r 
 |-  R = ( Scalar ` U )
6 dochkr1.z 
 |-  .0. = ( 0g ` U )
7 dochkr1.i 
 |-  .1. = ( 1r ` R )
8 dochkr1.f 
 |-  F = ( LFnl ` U )
9 dochkr1.l 
 |-  L = ( LKer ` U )
10 dochkr1.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
11 dochkr1.g 
 |-  ( ph -> G e. F )
12 dochkr1.n 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V )
13 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
14 eqid 
 |-  ( LSAtoms ` U ) = ( LSAtoms ` U )
15 1 3 10 dvhlmod 
 |-  ( ph -> U e. LMod )
16 1 2 3 4 14 8 9 10 11 dochkrsat2 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V <-> ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) )
17 12 16 mpbid 
 |-  ( ph -> ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) )
18 13 14 15 17 lsateln0 
 |-  ( ph -> E. z e. ( ._|_ ` ( L ` G ) ) z =/= ( 0g ` U ) )
19 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
20 10 ad2antrr 
 |-  ( ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) ) /\ z =/= ( 0g ` U ) ) -> ( K e. HL /\ W e. H ) )
21 11 ad2antrr 
 |-  ( ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) ) /\ z =/= ( 0g ` U ) ) -> G e. F )
22 eldifsn 
 |-  ( z e. ( ( ._|_ ` ( L ` G ) ) \ { ( 0g ` U ) } ) <-> ( z e. ( ._|_ ` ( L ` G ) ) /\ z =/= ( 0g ` U ) ) )
23 22 biimpri 
 |-  ( ( z e. ( ._|_ ` ( L ` G ) ) /\ z =/= ( 0g ` U ) ) -> z e. ( ( ._|_ ` ( L ` G ) ) \ { ( 0g ` U ) } ) )
24 23 adantll 
 |-  ( ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) ) /\ z =/= ( 0g ` U ) ) -> z e. ( ( ._|_ ` ( L ` G ) ) \ { ( 0g ` U ) } ) )
25 1 2 3 4 5 19 13 8 9 20 21 24 dochfln0 
 |-  ( ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) ) /\ z =/= ( 0g ` U ) ) -> ( G ` z ) =/= ( 0g ` R ) )
26 25 ex 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) ) -> ( z =/= ( 0g ` U ) -> ( G ` z ) =/= ( 0g ` R ) ) )
27 26 reximdva 
 |-  ( ph -> ( E. z e. ( ._|_ ` ( L ` G ) ) z =/= ( 0g ` U ) -> E. z e. ( ._|_ ` ( L ` G ) ) ( G ` z ) =/= ( 0g ` R ) ) )
28 18 27 mpd 
 |-  ( ph -> E. z e. ( ._|_ ` ( L ` G ) ) ( G ` z ) =/= ( 0g ` R ) )
29 4 8 9 15 11 lkrssv 
 |-  ( ph -> ( L ` G ) C_ V )
30 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
31 1 3 4 30 2 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( L ` G ) C_ V ) -> ( ._|_ ` ( L ` G ) ) e. ( LSubSp ` U ) )
32 10 29 31 syl2anc 
 |-  ( ph -> ( ._|_ ` ( L ` G ) ) e. ( LSubSp ` U ) )
33 15 32 jca 
 |-  ( ph -> ( U e. LMod /\ ( ._|_ ` ( L ` G ) ) e. ( LSubSp ` U ) ) )
34 33 3ad2ant1 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> ( U e. LMod /\ ( ._|_ ` ( L ` G ) ) e. ( LSubSp ` U ) ) )
35 1 3 10 dvhlvec 
 |-  ( ph -> U e. LVec )
36 35 3ad2ant1 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> U e. LVec )
37 5 lvecdrng 
 |-  ( U e. LVec -> R e. DivRing )
38 36 37 syl 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> R e. DivRing )
39 15 3ad2ant1 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> U e. LMod )
40 11 3ad2ant1 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> G e. F )
41 1 3 4 2 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( L ` G ) C_ V ) -> ( ._|_ ` ( L ` G ) ) C_ V )
42 10 29 41 syl2anc 
 |-  ( ph -> ( ._|_ ` ( L ` G ) ) C_ V )
43 42 sselda 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) ) -> z e. V )
44 43 3adant3 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> z e. V )
45 eqid 
 |-  ( Base ` R ) = ( Base ` R )
46 5 45 4 8 lflcl 
 |-  ( ( U e. LMod /\ G e. F /\ z e. V ) -> ( G ` z ) e. ( Base ` R ) )
47 39 40 44 46 syl3anc 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> ( G ` z ) e. ( Base ` R ) )
48 simp3 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> ( G ` z ) =/= ( 0g ` R ) )
49 eqid 
 |-  ( invr ` R ) = ( invr ` R )
50 45 19 49 drnginvrcl 
 |-  ( ( R e. DivRing /\ ( G ` z ) e. ( Base ` R ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> ( ( invr ` R ) ` ( G ` z ) ) e. ( Base ` R ) )
51 38 47 48 50 syl3anc 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> ( ( invr ` R ) ` ( G ` z ) ) e. ( Base ` R ) )
52 simp2 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> z e. ( ._|_ ` ( L ` G ) ) )
53 51 52 jca 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> ( ( ( invr ` R ) ` ( G ` z ) ) e. ( Base ` R ) /\ z e. ( ._|_ ` ( L ` G ) ) ) )
54 eqid 
 |-  ( .s ` U ) = ( .s ` U )
55 5 54 45 30 lssvscl 
 |-  ( ( ( U e. LMod /\ ( ._|_ ` ( L ` G ) ) e. ( LSubSp ` U ) ) /\ ( ( ( invr ` R ) ` ( G ` z ) ) e. ( Base ` R ) /\ z e. ( ._|_ ` ( L ` G ) ) ) ) -> ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) e. ( ._|_ ` ( L ` G ) ) )
56 34 53 55 syl2anc 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) e. ( ._|_ ` ( L ` G ) ) )
57 45 19 49 drnginvrn0 
 |-  ( ( R e. DivRing /\ ( G ` z ) e. ( Base ` R ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> ( ( invr ` R ) ` ( G ` z ) ) =/= ( 0g ` R ) )
58 38 47 48 57 syl3anc 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> ( ( invr ` R ) ` ( G ` z ) ) =/= ( 0g ` R ) )
59 15 adantr 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) ) -> U e. LMod )
60 11 adantr 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) ) -> G e. F )
61 5 19 6 8 lfl0 
 |-  ( ( U e. LMod /\ G e. F ) -> ( G ` .0. ) = ( 0g ` R ) )
62 59 60 61 syl2anc 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) ) -> ( G ` .0. ) = ( 0g ` R ) )
63 fveqeq2 
 |-  ( z = .0. -> ( ( G ` z ) = ( 0g ` R ) <-> ( G ` .0. ) = ( 0g ` R ) ) )
64 62 63 syl5ibrcom 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) ) -> ( z = .0. -> ( G ` z ) = ( 0g ` R ) ) )
65 64 necon3d 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) ) -> ( ( G ` z ) =/= ( 0g ` R ) -> z =/= .0. ) )
66 65 3impia 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> z =/= .0. )
67 4 54 5 45 19 6 36 51 44 lvecvsn0 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> ( ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) =/= .0. <-> ( ( ( invr ` R ) ` ( G ` z ) ) =/= ( 0g ` R ) /\ z =/= .0. ) ) )
68 58 66 67 mpbir2and 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) =/= .0. )
69 eldifsn 
 |-  ( ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) <-> ( ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) e. ( ._|_ ` ( L ` G ) ) /\ ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) =/= .0. ) )
70 56 68 69 sylanbrc 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )
71 eqid 
 |-  ( .r ` R ) = ( .r ` R )
72 5 45 71 4 54 8 lflmul 
 |-  ( ( U e. LMod /\ G e. F /\ ( ( ( invr ` R ) ` ( G ` z ) ) e. ( Base ` R ) /\ z e. V ) ) -> ( G ` ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) ) = ( ( ( invr ` R ) ` ( G ` z ) ) ( .r ` R ) ( G ` z ) ) )
73 39 40 51 44 72 syl112anc 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> ( G ` ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) ) = ( ( ( invr ` R ) ` ( G ` z ) ) ( .r ` R ) ( G ` z ) ) )
74 45 19 71 7 49 drnginvrl 
 |-  ( ( R e. DivRing /\ ( G ` z ) e. ( Base ` R ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> ( ( ( invr ` R ) ` ( G ` z ) ) ( .r ` R ) ( G ` z ) ) = .1. )
75 38 47 48 74 syl3anc 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> ( ( ( invr ` R ) ` ( G ` z ) ) ( .r ` R ) ( G ` z ) ) = .1. )
76 73 75 eqtrd 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> ( G ` ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) ) = .1. )
77 fveqeq2 
 |-  ( x = ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) -> ( ( G ` x ) = .1. <-> ( G ` ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) ) = .1. ) )
78 77 rspcev 
 |-  ( ( ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) /\ ( G ` ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) ) = .1. ) -> E. x e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) ( G ` x ) = .1. )
79 70 76 78 syl2anc 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= ( 0g ` R ) ) -> E. x e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) ( G ` x ) = .1. )
80 79 rexlimdv3a 
 |-  ( ph -> ( E. z e. ( ._|_ ` ( L ` G ) ) ( G ` z ) =/= ( 0g ` R ) -> E. x e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) ( G ` x ) = .1. ) )
81 28 80 mpd 
 |-  ( ph -> E. x e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) ( G ` x ) = .1. )