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

Theorem lfl1 29805
 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 2602 . . . . . . 7
21ralbii 2721 . . . . . 6
3 lfl1.d . . . . . . . . . 10 Scalar
4 eqid 2435 . . . . . . . . . 10
5 lfl1.v . . . . . . . . . 10
6 lfl1.f . . . . . . . . . 10 LFnl
73, 4, 5, 6lflf 29798 . . . . . . . . 9
8 ffn 5583 . . . . . . . . 9
97, 8syl 16 . . . . . . . 8
10 fconstfv 5946 . . . . . . . . 9
1110simplbi2 609 . . . . . . . 8
129, 11syl 16 . . . . . . 7
13 lfl1.o . . . . . . . . 9
14 fvex 5734 . . . . . . . . 9
1513, 14eqeltri 2505 . . . . . . . 8
1615fconst2 5940 . . . . . . 7
1712, 16syl6ib 218 . . . . . 6
182, 17syl5bi 209 . . . . 5
1918necon3ad 2634 . . . 4
20 dfrex2 2710 . . . 4
2119, 20syl6ibr 219 . . 3
22213impia 1150 . 2
23 simp1l 981 . . . . . . 7
24 lveclmod 16170 . . . . . . 7
2523, 24syl 16 . . . . . 6
263lvecdrng 16169 . . . . . . . 8
2723, 26syl 16 . . . . . . 7
28 simp1r 982 . . . . . . . 8
29 simp2 958 . . . . . . . 8
303, 4, 5, 6lflcl 29799 . . . . . . . 8
3123, 28, 29, 30syl3anc 1184 . . . . . . 7
32 simp3 959 . . . . . . 7
33 eqid 2435 . . . . . . . 8
344, 13, 33drnginvrcl 15844 . . . . . . 7
3527, 31, 32, 34syl3anc 1184 . . . . . 6
36 eqid 2435 . . . . . . 7
375, 3, 36, 4lmodvscl 15959 . . . . . 6
3825, 35, 29, 37syl3anc 1184 . . . . 5
39 eqid 2435 . . . . . . . 8
403, 4, 39, 5, 36, 6lflmul 29803 . . . . . . 7
4125, 28, 35, 29, 40syl112anc 1188 . . . . . 6
42 lfl1.u . . . . . . . 8
434, 13, 39, 42, 33drnginvrl 15846 . . . . . . 7
4427, 31, 32, 43syl3anc 1184 . . . . . 6
4541, 44eqtrd 2467 . . . . 5
46 fveq2 5720 . . . . . . 7
4746eqeq1d 2443 . . . . . 6
4847rspcev 3044 . . . . 5
4938, 45, 48syl2anc 643 . . . 4
5049rexlimdv3a 2824 . . 3