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=ScalarW
lfl1.o 0˙=0D
lfl1.u 1˙=1D
lfl1.v V=BaseW
lfl1.f F=LFnlW
Assertion lfl1 WLVecGFGV×0˙xVGx=1˙

Proof

Step Hyp Ref Expression
1 lfl1.d D=ScalarW
2 lfl1.o 0˙=0D
3 lfl1.u 1˙=1D
4 lfl1.v V=BaseW
5 lfl1.f F=LFnlW
6 nne ¬Gz0˙Gz=0˙
7 6 ralbii zV¬Gz0˙zVGz=0˙
8 eqid BaseD=BaseD
9 1 8 4 5 lflf WLVecGFG:VBaseD
10 9 ffnd WLVecGFGFnV
11 fconstfv G:V0˙GFnVzVGz=0˙
12 11 simplbi2 GFnVzVGz=0˙G:V0˙
13 10 12 syl WLVecGFzVGz=0˙G:V0˙
14 2 fvexi 0˙V
15 14 fconst2 G:V0˙G=V×0˙
16 13 15 syl6ib WLVecGFzVGz=0˙G=V×0˙
17 7 16 syl5bi WLVecGFzV¬Gz0˙G=V×0˙
18 17 necon3ad WLVecGFGV×0˙¬zV¬Gz0˙
19 dfrex2 zVGz0˙¬zV¬Gz0˙
20 18 19 syl6ibr WLVecGFGV×0˙zVGz0˙
21 20 3impia WLVecGFGV×0˙zVGz0˙
22 simp1l WLVecGFzVGz0˙WLVec
23 lveclmod WLVecWLMod
24 22 23 syl WLVecGFzVGz0˙WLMod
25 1 lvecdrng WLVecDDivRing
26 22 25 syl WLVecGFzVGz0˙DDivRing
27 simp1r WLVecGFzVGz0˙GF
28 simp2 WLVecGFzVGz0˙zV
29 1 8 4 5 lflcl WLVecGFzVGzBaseD
30 22 27 28 29 syl3anc WLVecGFzVGz0˙GzBaseD
31 simp3 WLVecGFzVGz0˙Gz0˙
32 eqid invrD=invrD
33 8 2 32 drnginvrcl DDivRingGzBaseDGz0˙invrDGzBaseD
34 26 30 31 33 syl3anc WLVecGFzVGz0˙invrDGzBaseD
35 eqid W=W
36 4 1 35 8 lmodvscl WLModinvrDGzBaseDzVinvrDGzWzV
37 24 34 28 36 syl3anc WLVecGFzVGz0˙invrDGzWzV
38 eqid D=D
39 1 8 38 4 35 5 lflmul WLModGFinvrDGzBaseDzVGinvrDGzWz=invrDGzDGz
40 24 27 34 28 39 syl112anc WLVecGFzVGz0˙GinvrDGzWz=invrDGzDGz
41 8 2 38 3 32 drnginvrl DDivRingGzBaseDGz0˙invrDGzDGz=1˙
42 26 30 31 41 syl3anc WLVecGFzVGz0˙invrDGzDGz=1˙
43 40 42 eqtrd WLVecGFzVGz0˙GinvrDGzWz=1˙
44 fveqeq2 x=invrDGzWzGx=1˙GinvrDGzWz=1˙
45 44 rspcev invrDGzWzVGinvrDGzWz=1˙xVGx=1˙
46 37 43 45 syl2anc WLVecGFzVGz0˙xVGx=1˙
47 46 rexlimdv3a WLVecGFzVGz0˙xVGx=1˙
48 47 3adant3 WLVecGFGV×0˙zVGz0˙xVGx=1˙
49 21 48 mpd WLVecGFGV×0˙xVGx=1˙