Metamath Proof Explorer

Theorem curf12

Description: The partially evaluated curry functor at a morphism. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses curfval.g 
|- G = ( <. C , D >. curryF F )
curfval.a 
|- A = ( Base ` C )
curfval.c 
|- ( ph -> C e. Cat )
curfval.d 
|- ( ph -> D e. Cat )
curfval.f 
|- ( ph -> F e. ( ( C Xc. D ) Func E ) )
curfval.b 
|- B = ( Base ` D )
curf1.x 
|- ( ph -> X e. A )
curf1.k 
|- K = ( ( 1st ` G ) ` X )
curf11.y 
|- ( ph -> Y e. B )
curf12.j 
|- J = ( Hom ` D )
curf12.1 
|- .1. = ( Id ` C )
curf12.y 
|- ( ph -> Z e. B )
curf12.g 
|- ( ph -> H e. ( Y J Z ) )
Assertion curf12 
|- ( ph -> ( ( Y ( 2nd ` K ) Z ) ` H ) = ( ( .1. ` X ) ( <. X , Y >. ( 2nd ` F ) <. X , Z >. ) H ) )

Proof

Step Hyp Ref Expression
1 curfval.g 
 |-  G = ( <. C , D >. curryF F )
2 curfval.a 
 |-  A = ( Base ` C )
3 curfval.c 
 |-  ( ph -> C e. Cat )
4 curfval.d 
 |-  ( ph -> D e. Cat )
5 curfval.f 
 |-  ( ph -> F e. ( ( C Xc. D ) Func E ) )
6 curfval.b 
 |-  B = ( Base ` D )
7 curf1.x 
 |-  ( ph -> X e. A )
8 curf1.k 
 |-  K = ( ( 1st ` G ) ` X )
9 curf11.y 
 |-  ( ph -> Y e. B )
10 curf12.j 
 |-  J = ( Hom ` D )
11 curf12.1 
 |-  .1. = ( Id ` C )
12 curf12.y 
 |-  ( ph -> Z e. B )
13 curf12.g 
 |-  ( ph -> H e. ( Y J Z ) )
14 1 2 3 4 5 6 7 8 10 11 curf1 
 |-  ( ph -> K = <. ( y e. B |-> ( X ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) >. )
15 6 fvexi 
 |-  B e. _V
16 15 mptex 
 |-  ( y e. B |-> ( X ( 1st ` F ) y ) ) e. _V
17 15 15 mpoex 
 |-  ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) e. _V
18 16 17 op2ndd 
 |-  ( K = <. ( y e. B |-> ( X ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) >. -> ( 2nd ` K ) = ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) )
19 14 18 syl 
 |-  ( ph -> ( 2nd ` K ) = ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) )
20 12 adantr 
 |-  ( ( ph /\ y = Y ) -> Z e. B )
21 ovex 
 |-  ( y J z ) e. _V
22 21 mptex 
 |-  ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) e. _V
23 22 a1i 
 |-  ( ( ph /\ ( y = Y /\ z = Z ) ) -> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) e. _V )
24 13 adantr 
 |-  ( ( ph /\ ( y = Y /\ z = Z ) ) -> H e. ( Y J Z ) )
25 simprl 
 |-  ( ( ph /\ ( y = Y /\ z = Z ) ) -> y = Y )
26 simprr 
 |-  ( ( ph /\ ( y = Y /\ z = Z ) ) -> z = Z )
27 25 26 oveq12d 
 |-  ( ( ph /\ ( y = Y /\ z = Z ) ) -> ( y J z ) = ( Y J Z ) )
28 24 27 eleqtrrd 
 |-  ( ( ph /\ ( y = Y /\ z = Z ) ) -> H e. ( y J z ) )
29 ovexd 
 |-  ( ( ( ph /\ ( y = Y /\ z = Z ) ) /\ g = H ) -> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) e. _V )
30 simplrl 
 |-  ( ( ( ph /\ ( y = Y /\ z = Z ) ) /\ g = H ) -> y = Y )
31 30 opeq2d 
 |-  ( ( ( ph /\ ( y = Y /\ z = Z ) ) /\ g = H ) -> <. X , y >. = <. X , Y >. )
32 simplrr 
 |-  ( ( ( ph /\ ( y = Y /\ z = Z ) ) /\ g = H ) -> z = Z )
33 32 opeq2d 
 |-  ( ( ( ph /\ ( y = Y /\ z = Z ) ) /\ g = H ) -> <. X , z >. = <. X , Z >. )
34 31 33 oveq12d 
 |-  ( ( ( ph /\ ( y = Y /\ z = Z ) ) /\ g = H ) -> ( <. X , y >. ( 2nd ` F ) <. X , z >. ) = ( <. X , Y >. ( 2nd ` F ) <. X , Z >. ) )
35 eqidd 
 |-  ( ( ( ph /\ ( y = Y /\ z = Z ) ) /\ g = H ) -> ( .1. ` X ) = ( .1. ` X ) )
36 simpr 
 |-  ( ( ( ph /\ ( y = Y /\ z = Z ) ) /\ g = H ) -> g = H )
37 34 35 36 oveq123d 
 |-  ( ( ( ph /\ ( y = Y /\ z = Z ) ) /\ g = H ) -> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) = ( ( .1. ` X ) ( <. X , Y >. ( 2nd ` F ) <. X , Z >. ) H ) )
38 28 29 37 fvmptdv2 
 |-  ( ( ph /\ ( y = Y /\ z = Z ) ) -> ( ( Y ( 2nd ` K ) Z ) = ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) -> ( ( Y ( 2nd ` K ) Z ) ` H ) = ( ( .1. ` X ) ( <. X , Y >. ( 2nd ` F ) <. X , Z >. ) H ) ) )
39 9 20 23 38 ovmpodv 
 |-  ( ph -> ( ( 2nd ` K ) = ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) -> ( ( Y ( 2nd ` K ) Z ) ` H ) = ( ( .1. ` X ) ( <. X , Y >. ( 2nd ` F ) <. X , Z >. ) H ) ) )
40 19 39 mpd 
 |-  ( ph -> ( ( Y ( 2nd ` K ) Z ) ` H ) = ( ( .1. ` X ) ( <. X , Y >. ( 2nd ` F ) <. X , Z >. ) H ) )