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

Metamath Proof Explorer

Theorem dochkr1OLDN

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) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 dochkr1OLD.h 
 |-  H = ( LHyp ` K )
2 dochkr1OLD.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 dochkr1OLD.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 dochkr1OLD.v 
 |-  V = ( Base ` U )
5 dochkr1OLD.r 
 |-  R = ( Scalar ` U )
6 dochkr1OLD.z 
 |-  .0. = ( 0g ` R )
7 dochkr1OLD.i 
 |-  .1. = ( 1r ` R )
8 dochkr1OLD.f 
 |-  F = ( LFnl ` U )
9 dochkr1OLD.l 
 |-  L = ( LKer ` U )
10 dochkr1OLD.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
11 dochkr1OLD.g 
 |-  ( ph -> G e. F )
12 dochkr1OLD.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 10 ad2antrr 
 |-  ( ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) ) /\ z =/= ( 0g ` U ) ) -> ( K e. HL /\ W e. H ) )
20 11 ad2antrr 
 |-  ( ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) ) /\ z =/= ( 0g ` U ) ) -> G e. F )
21 eldifsn 
 |-  ( z e. ( ( ._|_ ` ( L ` G ) ) \ { ( 0g ` U ) } ) <-> ( z e. ( ._|_ ` ( L ` G ) ) /\ z =/= ( 0g ` U ) ) )
22 21 biimpri 
 |-  ( ( z e. ( ._|_ ` ( L ` G ) ) /\ z =/= ( 0g ` U ) ) -> z e. ( ( ._|_ ` ( L ` G ) ) \ { ( 0g ` U ) } ) )
23 22 adantll 
 |-  ( ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) ) /\ z =/= ( 0g ` U ) ) -> z e. ( ( ._|_ ` ( L ` G ) ) \ { ( 0g ` U ) } ) )
24 1 2 3 4 5 6 13 8 9 19 20 23 dochfln0 
 |-  ( ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) ) /\ z =/= ( 0g ` U ) ) -> ( G ` z ) =/= .0. )
25 24 ex 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) ) -> ( z =/= ( 0g ` U ) -> ( G ` z ) =/= .0. ) )
26 25 reximdva 
 |-  ( ph -> ( E. z e. ( ._|_ ` ( L ` G ) ) z =/= ( 0g ` U ) -> E. z e. ( ._|_ ` ( L ` G ) ) ( G ` z ) =/= .0. ) )
27 18 26 mpd 
 |-  ( ph -> E. z e. ( ._|_ ` ( L ` G ) ) ( G ` z ) =/= .0. )
28 4 8 9 15 11 lkrssv 
 |-  ( ph -> ( L ` G ) C_ V )
29 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
30 1 3 4 29 2 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( L ` G ) C_ V ) -> ( ._|_ ` ( L ` G ) ) e. ( LSubSp ` U ) )
31 10 28 30 syl2anc 
 |-  ( ph -> ( ._|_ ` ( L ` G ) ) e. ( LSubSp ` U ) )
32 15 31 jca 
 |-  ( ph -> ( U e. LMod /\ ( ._|_ ` ( L ` G ) ) e. ( LSubSp ` U ) ) )
33 32 3ad2ant1 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= .0. ) -> ( U e. LMod /\ ( ._|_ ` ( L ` G ) ) e. ( LSubSp ` U ) ) )
34 1 3 10 dvhlvec 
 |-  ( ph -> U e. LVec )
35 34 3ad2ant1 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= .0. ) -> U e. LVec )
36 5 lvecdrng 
 |-  ( U e. LVec -> R e. DivRing )
37 35 36 syl 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= .0. ) -> R e. DivRing )
38 15 3ad2ant1 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= .0. ) -> U e. LMod )
39 11 3ad2ant1 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= .0. ) -> G e. F )
40 1 3 4 2 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( L ` G ) C_ V ) -> ( ._|_ ` ( L ` G ) ) C_ V )
41 10 28 40 syl2anc 
 |-  ( ph -> ( ._|_ ` ( L ` G ) ) C_ V )
42 41 sselda 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) ) -> z e. V )
43 42 3adant3 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= .0. ) -> z e. V )
44 eqid 
 |-  ( Base ` R ) = ( Base ` R )
45 5 44 4 8 lflcl 
 |-  ( ( U e. LMod /\ G e. F /\ z e. V ) -> ( G ` z ) e. ( Base ` R ) )
46 38 39 43 45 syl3anc 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= .0. ) -> ( G ` z ) e. ( Base ` R ) )
47 simp3 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= .0. ) -> ( G ` z ) =/= .0. )
48 eqid 
 |-  ( invr ` R ) = ( invr ` R )
49 44 6 48 drnginvrcl 
 |-  ( ( R e. DivRing /\ ( G ` z ) e. ( Base ` R ) /\ ( G ` z ) =/= .0. ) -> ( ( invr ` R ) ` ( G ` z ) ) e. ( Base ` R ) )
50 37 46 47 49 syl3anc 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= .0. ) -> ( ( invr ` R ) ` ( G ` z ) ) e. ( Base ` R ) )
51 simp2 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= .0. ) -> z e. ( ._|_ ` ( L ` G ) ) )
52 eqid 
 |-  ( .s ` U ) = ( .s ` U )
53 5 52 44 29 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 ) ) )
54 33 50 51 53 syl12anc 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= .0. ) -> ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) e. ( ._|_ ` ( L ` G ) ) )
55 eqid 
 |-  ( .r ` R ) = ( .r ` R )
56 5 44 55 4 52 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 ) ) )
57 38 39 50 43 56 syl112anc 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= .0. ) -> ( G ` ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) ) = ( ( ( invr ` R ) ` ( G ` z ) ) ( .r ` R ) ( G ` z ) ) )
58 44 6 55 7 48 drnginvrl 
 |-  ( ( R e. DivRing /\ ( G ` z ) e. ( Base ` R ) /\ ( G ` z ) =/= .0. ) -> ( ( ( invr ` R ) ` ( G ` z ) ) ( .r ` R ) ( G ` z ) ) = .1. )
59 37 46 47 58 syl3anc 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= .0. ) -> ( ( ( invr ` R ) ` ( G ` z ) ) ( .r ` R ) ( G ` z ) ) = .1. )
60 57 59 eqtrd 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= .0. ) -> ( G ` ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) ) = .1. )
61 fveqeq2 
 |-  ( x = ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) -> ( ( G ` x ) = .1. <-> ( G ` ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) ) = .1. ) )
62 61 rspcev 
 |-  ( ( ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) e. ( ._|_ ` ( L ` G ) ) /\ ( G ` ( ( ( invr ` R ) ` ( G ` z ) ) ( .s ` U ) z ) ) = .1. ) -> E. x e. ( ._|_ ` ( L ` G ) ) ( G ` x ) = .1. )
63 54 60 62 syl2anc 
 |-  ( ( ph /\ z e. ( ._|_ ` ( L ` G ) ) /\ ( G ` z ) =/= .0. ) -> E. x e. ( ._|_ ` ( L ` G ) ) ( G ` x ) = .1. )
64 63 rexlimdv3a 
 |-  ( ph -> ( E. z e. ( ._|_ ` ( L ` G ) ) ( G ` z ) =/= .0. -> E. x e. ( ._|_ ` ( L ` G ) ) ( G ` x ) = .1. ) )
65 27 64 mpd 
 |-  ( ph -> E. x e. ( ._|_ ` ( L ` G ) ) ( G ` x ) = .1. )