Step |
Hyp |
Ref |
Expression |
1 |
|
evlfval.e |
|- E = ( C evalF D ) |
2 |
|
evlfval.c |
|- ( ph -> C e. Cat ) |
3 |
|
evlfval.d |
|- ( ph -> D e. Cat ) |
4 |
|
evlfval.b |
|- B = ( Base ` C ) |
5 |
|
evlfval.h |
|- H = ( Hom ` C ) |
6 |
|
evlfval.o |
|- .x. = ( comp ` D ) |
7 |
|
evlfval.n |
|- N = ( C Nat D ) |
8 |
|
evlf2.f |
|- ( ph -> F e. ( C Func D ) ) |
9 |
|
evlf2.g |
|- ( ph -> G e. ( C Func D ) ) |
10 |
|
evlf2.x |
|- ( ph -> X e. B ) |
11 |
|
evlf2.y |
|- ( ph -> Y e. B ) |
12 |
|
evlf2.l |
|- L = ( <. F , X >. ( 2nd ` E ) <. G , Y >. ) |
13 |
|
evlf2val.a |
|- ( ph -> A e. ( F N G ) ) |
14 |
|
evlf2val.k |
|- ( ph -> K e. ( X H Y ) ) |
15 |
1 2 3 4 5 6 7 8 9 10 11 12
|
evlf2 |
|- ( ph -> L = ( a e. ( F N G ) , g e. ( X H Y ) |-> ( ( a ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` g ) ) ) ) |
16 |
|
simprl |
|- ( ( ph /\ ( a = A /\ g = K ) ) -> a = A ) |
17 |
16
|
fveq1d |
|- ( ( ph /\ ( a = A /\ g = K ) ) -> ( a ` Y ) = ( A ` Y ) ) |
18 |
|
simprr |
|- ( ( ph /\ ( a = A /\ g = K ) ) -> g = K ) |
19 |
18
|
fveq2d |
|- ( ( ph /\ ( a = A /\ g = K ) ) -> ( ( X ( 2nd ` F ) Y ) ` g ) = ( ( X ( 2nd ` F ) Y ) ` K ) ) |
20 |
17 19
|
oveq12d |
|- ( ( ph /\ ( a = A /\ g = K ) ) -> ( ( a ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` g ) ) = ( ( A ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) ) |
21 |
|
ovexd |
|- ( ph -> ( ( A ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) e. _V ) |
22 |
15 20 13 14 21
|
ovmpod |
|- ( ph -> ( A L K ) = ( ( A ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) ) |