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 syl6ib
 |-  ( ( W e. LVec /\ G e. F ) -> ( A. z e. V ( G ` z ) = .0. -> G = ( V X. { .0. } ) ) )
17 7 16 syl5bi
 |-  ( ( 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 syl6ibr
 |-  ( ( 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. )