Metamath Proof Explorer

Theorem lfl1

Description: A nonzero functional has a value of 1 at some argument. (Contributed by NM, 16-Apr-2014)

Ref Expression
Hypotheses lfl1.d 
|- D = ( Scalar ` W )
lfl1.o 
|- .0. = ( 0g ` D )
lfl1.u 
|- .1. = ( 1r ` D )
lfl1.v 
|- V = ( Base ` W )
lfl1.f 
|- F = ( LFnl ` W )
Assertion lfl1 
|- ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> E. x e. V ( G ` x ) = .1. )

Proof

Step Hyp Ref Expression
1 lfl1.d 
 |-  D = ( Scalar ` W )
2 lfl1.o 
 |-  .0. = ( 0g ` D )
3 lfl1.u 
 |-  .1. = ( 1r ` D )
4 lfl1.v 
 |-  V = ( Base ` W )
5 lfl1.f 
 |-  F = ( LFnl ` W )
6 nne 
 |-  ( -. ( G ` z ) =/= .0. <-> ( G ` z ) = .0. )
7 6 ralbii 
 |-  ( A. z e. V -. ( G ` z ) =/= .0. <-> A. z e. V ( G ` z ) = .0. )
8 eqid 
 |-  ( Base ` D ) = ( Base ` D )
9 1 8 4 5 lflf 
 |-  ( ( W e. LVec /\ G e. F ) -> G : V --> ( Base ` D ) )
10 9 ffnd 
 |-  ( ( W e. LVec /\ G e. F ) -> G Fn V )
11 fconstfv 
 |-  ( G : V --> { .0. } <-> ( G Fn V /\ A. z e. V ( G ` z ) = .0. ) )
12 11 simplbi2 
 |-  ( G Fn V -> ( A. z e. V ( G ` z ) = .0. -> G : V --> { .0. } ) )
13 10 12 syl 
 |-  ( ( W e. LVec /\ G e. F ) -> ( A. z e. V ( G ` z ) = .0. -> G : V --> { .0. } ) )
14 2 fvexi 
 |-  .0. e. _V
15 14 fconst2 
 |-  ( G : V --> { .0. } <-> G = ( V X. { .0. } ) )
16 13 15 imbitrdi 
 |-  ( ( W e. LVec /\ G e. F ) -> ( A. z e. V ( G ` z ) = .0. -> G = ( V X. { .0. } ) ) )
17 7 16 biimtrid 
 |-  ( ( W e. LVec /\ G e. F ) -> ( A. z e. V -. ( G ` z ) =/= .0. -> G = ( V X. { .0. } ) ) )
18 17 necon3ad 
 |-  ( ( W e. LVec /\ G e. F ) -> ( G =/= ( V X. { .0. } ) -> -. A. z e. V -. ( G ` z ) =/= .0. ) )
19 dfrex2 
 |-  ( E. z e. V ( G ` z ) =/= .0. <-> -. A. z e. V -. ( G ` z ) =/= .0. )
20 18 19 imbitrrdi 
 |-  ( ( W e. LVec /\ G e. F ) -> ( G =/= ( V X. { .0. } ) -> E. z e. V ( G ` z ) =/= .0. ) )
21 20 3impia 
 |-  ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> E. z e. V ( G ` z ) =/= .0. )
22 simp1l 
 |-  ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> W e. LVec )
23 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
24 22 23 syl 
 |-  ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> W e. LMod )
25 1 lvecdrng 
 |-  ( W e. LVec -> D e. DivRing )
26 22 25 syl 
 |-  ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> D e. DivRing )
27 simp1r 
 |-  ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> G e. F )
28 simp2 
 |-  ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> z e. V )
29 1 8 4 5 lflcl 
 |-  ( ( W e. LVec /\ G e. F /\ z e. V ) -> ( G ` z ) e. ( Base ` D ) )
30 22 27 28 29 syl3anc 
 |-  ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> ( G ` z ) e. ( Base ` D ) )
31 simp3 
 |-  ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> ( G ` z ) =/= .0. )
32 eqid 
 |-  ( invr ` D ) = ( invr ` D )
33 8 2 32 drnginvrcl 
 |-  ( ( D e. DivRing /\ ( G ` z ) e. ( Base ` D ) /\ ( G ` z ) =/= .0. ) -> ( ( invr ` D ) ` ( G ` z ) ) e. ( Base ` D ) )
34 26 30 31 33 syl3anc 
 |-  ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> ( ( invr ` D ) ` ( G ` z ) ) e. ( Base ` D ) )
35 eqid 
 |-  ( .s ` W ) = ( .s ` W )
36 4 1 35 8 lmodvscl 
 |-  ( ( W e. LMod /\ ( ( invr ` D ) ` ( G ` z ) ) e. ( Base ` D ) /\ z e. V ) -> ( ( ( invr ` D ) ` ( G ` z ) ) ( .s ` W ) z ) e. V )
37 24 34 28 36 syl3anc 
 |-  ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> ( ( ( invr ` D ) ` ( G ` z ) ) ( .s ` W ) z ) e. V )
38 eqid 
 |-  ( .r ` D ) = ( .r ` D )
39 1 8 38 4 35 5 lflmul 
 |-  ( ( W e. LMod /\ G e. F /\ ( ( ( invr ` D ) ` ( G ` z ) ) e. ( Base ` D ) /\ z e. V ) ) -> ( G ` ( ( ( invr ` D ) ` ( G ` z ) ) ( .s ` W ) z ) ) = ( ( ( invr ` D ) ` ( G ` z ) ) ( .r ` D ) ( G ` z ) ) )
40 24 27 34 28 39 syl112anc 
 |-  ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> ( G ` ( ( ( invr ` D ) ` ( G ` z ) ) ( .s ` W ) z ) ) = ( ( ( invr ` D ) ` ( G ` z ) ) ( .r ` D ) ( G ` z ) ) )
41 8 2 38 3 32 drnginvrl 
 |-  ( ( D e. DivRing /\ ( G ` z ) e. ( Base ` D ) /\ ( G ` z ) =/= .0. ) -> ( ( ( invr ` D ) ` ( G ` z ) ) ( .r ` D ) ( G ` z ) ) = .1. )
42 26 30 31 41 syl3anc 
 |-  ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> ( ( ( invr ` D ) ` ( G ` z ) ) ( .r ` D ) ( G ` z ) ) = .1. )
43 40 42 eqtrd 
 |-  ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> ( G ` ( ( ( invr ` D ) ` ( G ` z ) ) ( .s ` W ) z ) ) = .1. )
44 fveqeq2 
 |-  ( x = ( ( ( invr ` D ) ` ( G ` z ) ) ( .s ` W ) z ) -> ( ( G ` x ) = .1. <-> ( G ` ( ( ( invr ` D ) ` ( G ` z ) ) ( .s ` W ) z ) ) = .1. ) )
45 44 rspcev 
 |-  ( ( ( ( ( invr ` D ) ` ( G ` z ) ) ( .s ` W ) z ) e. V /\ ( G ` ( ( ( invr ` D ) ` ( G ` z ) ) ( .s ` W ) z ) ) = .1. ) -> E. x e. V ( G ` x ) = .1. )
46 37 43 45 syl2anc 
 |-  ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> E. x e. V ( G ` x ) = .1. )
47 46 rexlimdv3a 
 |-  ( ( W e. LVec /\ G e. F ) -> ( E. z e. V ( G ` z ) =/= .0. -> E. x e. V ( G ` x ) = .1. ) )
48 47 3adant3 
 |-  ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> ( E. z e. V ( G ` z ) =/= .0. -> E. x e. V ( G ` x ) = .1. ) )
49 21 48 mpd 
 |-  ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> E. x e. V ( G ` x ) = .1. )