Description: Value of the evaluation functor. (Contributed by Mario Carneiro, 12-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | evlfval.e | |
|
evlfval.c | |
||
evlfval.d | |
||
evlfval.b | |
||
evlfval.h | |
||
evlfval.o | |
||
evlfval.n | |
||
Assertion | evlfval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | evlfval.e | |
|
2 | evlfval.c | |
|
3 | evlfval.d | |
|
4 | evlfval.b | |
|
5 | evlfval.h | |
|
6 | evlfval.o | |
|
7 | evlfval.n | |
|
8 | df-evlf | |
|
9 | 8 | a1i | |
10 | simprl | |
|
11 | simprr | |
|
12 | 10 11 | oveq12d | |
13 | 10 | fveq2d | |
14 | 13 4 | eqtr4di | |
15 | eqidd | |
|
16 | 12 14 15 | mpoeq123dv | |
17 | 12 14 | xpeq12d | |
18 | 10 11 | oveq12d | |
19 | 18 7 | eqtr4di | |
20 | 19 | oveqd | |
21 | 10 | fveq2d | |
22 | 21 5 | eqtr4di | |
23 | 22 | oveqd | |
24 | 11 | fveq2d | |
25 | 24 6 | eqtr4di | |
26 | 25 | oveqd | |
27 | 26 | oveqd | |
28 | 20 23 27 | mpoeq123dv | |
29 | 28 | csbeq2dv | |
30 | 29 | csbeq2dv | |
31 | 17 17 30 | mpoeq123dv | |
32 | 16 31 | opeq12d | |
33 | opex | |
|
34 | 33 | a1i | |
35 | 9 32 2 3 34 | ovmpod | |
36 | 1 35 | eqtrid | |