Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lfl1 Structured version   Visualization version   Unicode version

Theorem lfl1 32707
 Description: A non-zero functional has a value of 1 at some argument. (Contributed by NM, 16-Apr-2014.)
Hypotheses
Ref Expression
lfl1.d Scalar
lfl1.o
lfl1.u
lfl1.v
lfl1.f LFnl
Assertion
Ref Expression
lfl1
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem lfl1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 nne 2647 . . . . . . 7
21ralbii 2823 . . . . . 6
3 lfl1.d . . . . . . . . . 10 Scalar
4 eqid 2471 . . . . . . . . . 10
5 lfl1.v . . . . . . . . . 10
6 lfl1.f . . . . . . . . . 10 LFnl
73, 4, 5, 6lflf 32700 . . . . . . . . 9
8 ffn 5739 . . . . . . . . 9
97, 8syl 17 . . . . . . . 8
10 fconstfv 6143 . . . . . . . . 9
1110simplbi2 637 . . . . . . . 8
129, 11syl 17 . . . . . . 7
13 lfl1.o . . . . . . . . 9
14 fvex 5889 . . . . . . . . 9
1513, 14eqeltri 2545 . . . . . . . 8
1615fconst2 6137 . . . . . . 7
1712, 16syl6ib 234 . . . . . 6
182, 17syl5bi 225 . . . . 5
1918necon3ad 2656 . . . 4
20 dfrex2 2837 . . . 4
2119, 20syl6ibr 235 . . 3
22213impia 1228 . 2
23 simp1l 1054 . . . . . . 7
24 lveclmod 18407 . . . . . . 7
2523, 24syl 17 . . . . . 6
263lvecdrng 18406 . . . . . . . 8
2723, 26syl 17 . . . . . . 7
28 simp1r 1055 . . . . . . . 8
29 simp2 1031 . . . . . . . 8
303, 4, 5, 6lflcl 32701 . . . . . . . 8
3123, 28, 29, 30syl3anc 1292 . . . . . . 7
32 simp3 1032 . . . . . . 7
33 eqid 2471 . . . . . . . 8
344, 13, 33drnginvrcl 18070 . . . . . . 7
3527, 31, 32, 34syl3anc 1292 . . . . . 6
36 eqid 2471 . . . . . . 7
375, 3, 36, 4lmodvscl 18186 . . . . . 6
3825, 35, 29, 37syl3anc 1292 . . . . 5
39 eqid 2471 . . . . . . . 8
403, 4, 39, 5, 36, 6lflmul 32705 . . . . . . 7
4125, 28, 35, 29, 40syl112anc 1296 . . . . . 6
42 lfl1.u . . . . . . . 8
434, 13, 39, 42, 33drnginvrl 18072 . . . . . . 7
4427, 31, 32, 43syl3anc 1292 . . . . . 6
4541, 44eqtrd 2505 . . . . 5
46 fveq2 5879 . . . . . . 7
4746eqeq1d 2473 . . . . . 6
4847rspcev 3136 . . . . 5
4938, 45, 48syl2anc 673 . . . 4
5049rexlimdv3a 2873 . . 3