Description: A nonzero functional has a value of 1 at some argument. (Contributed by NM, 16-Apr-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lfl1.d | |
|
lfl1.o | |
||
lfl1.u | |
||
lfl1.v | |
||
lfl1.f | |
||
Assertion | lfl1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lfl1.d | |
|
2 | lfl1.o | |
|
3 | lfl1.u | |
|
4 | lfl1.v | |
|
5 | lfl1.f | |
|
6 | nne | |
|
7 | 6 | ralbii | |
8 | eqid | |
|
9 | 1 8 4 5 | lflf | |
10 | 9 | ffnd | |
11 | fconstfv | |
|
12 | 11 | simplbi2 | |
13 | 10 12 | syl | |
14 | 2 | fvexi | |
15 | 14 | fconst2 | |
16 | 13 15 | syl6ib | |
17 | 7 16 | syl5bi | |
18 | 17 | necon3ad | |
19 | dfrex2 | |
|
20 | 18 19 | syl6ibr | |
21 | 20 | 3impia | |
22 | simp1l | |
|
23 | lveclmod | |
|
24 | 22 23 | syl | |
25 | 1 | lvecdrng | |
26 | 22 25 | syl | |
27 | simp1r | |
|
28 | simp2 | |
|
29 | 1 8 4 5 | lflcl | |
30 | 22 27 28 29 | syl3anc | |
31 | simp3 | |
|
32 | eqid | |
|
33 | 8 2 32 | drnginvrcl | |
34 | 26 30 31 33 | syl3anc | |
35 | eqid | |
|
36 | 4 1 35 8 | lmodvscl | |
37 | 24 34 28 36 | syl3anc | |
38 | eqid | |
|
39 | 1 8 38 4 35 5 | lflmul | |
40 | 24 27 34 28 39 | syl112anc | |
41 | 8 2 38 3 32 | drnginvrl | |
42 | 26 30 31 41 | syl3anc | |
43 | 40 42 | eqtrd | |
44 | fveqeq2 | |
|
45 | 44 | rspcev | |
46 | 37 43 45 | syl2anc | |
47 | 46 | rexlimdv3a | |
48 | 47 | 3adant3 | |
49 | 21 48 | mpd | |