Metamath Proof Explorer

Theorem uncf2

Description: Value of the uncurry functor on a morphism. (Contributed by Mario Carneiro, 13-Jan-2017)

Ref Expression
Hypotheses uncfval.g 
|- F = ( <" C D E "> uncurryF G )
uncfval.c 
|- ( ph -> D e. Cat )
uncfval.d 
|- ( ph -> E e. Cat )
uncfval.f 
|- ( ph -> G e. ( C Func ( D FuncCat E ) ) )
uncf1.a 
|- A = ( Base ` C )
uncf1.b 
|- B = ( Base ` D )
uncf1.x 
|- ( ph -> X e. A )
uncf1.y 
|- ( ph -> Y e. B )
uncf2.h 
|- H = ( Hom ` C )
uncf2.j 
|- J = ( Hom ` D )
uncf2.z 
|- ( ph -> Z e. A )
uncf2.w 
|- ( ph -> W e. B )
uncf2.r 
|- ( ph -> R e. ( X H Z ) )
uncf2.s 
|- ( ph -> S e. ( Y J W ) )
Assertion uncf2 
|- ( ph -> ( R ( <. X , Y >. ( 2nd ` F ) <. Z , W >. ) S ) = ( ( ( ( X ( 2nd ` G ) Z ) ` R ) ` W ) ( <. ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` Y ) , ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` W ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` Z ) ) ` W ) ) ( ( Y ( 2nd ` ( ( 1st ` G ) ` X ) ) W ) ` S ) ) )

Proof

Step Hyp Ref Expression
1 uncfval.g 
 |-  F = ( <" C D E "> uncurryF G )
2 uncfval.c 
 |-  ( ph -> D e. Cat )
3 uncfval.d 
 |-  ( ph -> E e. Cat )
4 uncfval.f 
 |-  ( ph -> G e. ( C Func ( D FuncCat E ) ) )
5 uncf1.a 
 |-  A = ( Base ` C )
6 uncf1.b 
 |-  B = ( Base ` D )
7 uncf1.x 
 |-  ( ph -> X e. A )
8 uncf1.y 
 |-  ( ph -> Y e. B )
9 uncf2.h 
 |-  H = ( Hom ` C )
10 uncf2.j 
 |-  J = ( Hom ` D )
11 uncf2.z 
 |-  ( ph -> Z e. A )
12 uncf2.w 
 |-  ( ph -> W e. B )
13 uncf2.r 
 |-  ( ph -> R e. ( X H Z ) )
14 uncf2.s 
 |-  ( ph -> S e. ( Y J W ) )
15 1 2 3 4 uncfval 
 |-  ( ph -> F = ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) )
16 15 fveq2d 
 |-  ( ph -> ( 2nd ` F ) = ( 2nd ` ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ) )
17 16 oveqd 
 |-  ( ph -> ( <. X , Y >. ( 2nd ` F ) <. Z , W >. ) = ( <. X , Y >. ( 2nd ` ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ) <. Z , W >. ) )
18 17 oveqd 
 |-  ( ph -> ( R ( <. X , Y >. ( 2nd ` F ) <. Z , W >. ) S ) = ( R ( <. X , Y >. ( 2nd ` ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ) <. Z , W >. ) S ) )
19 df-ov 
 |-  ( R ( <. X , Y >. ( 2nd ` ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ) <. Z , W >. ) S ) = ( ( <. X , Y >. ( 2nd ` ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ) <. Z , W >. ) ` <. R , S >. )
20 eqid 
 |-  ( C Xc. D ) = ( C Xc. D )
21 20 5 6 xpcbas 
 |-  ( A X. B ) = ( Base ` ( C Xc. D ) )
22 eqid 
 |-  ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) = ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) )
23 eqid 
 |-  ( ( D FuncCat E ) Xc. D ) = ( ( D FuncCat E ) Xc. D )
24 funcrcl 
 |-  ( G e. ( C Func ( D FuncCat E ) ) -> ( C e. Cat /\ ( D FuncCat E ) e. Cat ) )
25 4 24 syl 
 |-  ( ph -> ( C e. Cat /\ ( D FuncCat E ) e. Cat ) )
26 25 simpld 
 |-  ( ph -> C e. Cat )
27 eqid 
 |-  ( C 1stF D ) = ( C 1stF D )
28 20 26 2 27 1stfcl 
 |-  ( ph -> ( C 1stF D ) e. ( ( C Xc. D ) Func C ) )
29 28 4 cofucl 
 |-  ( ph -> ( G o.func ( C 1stF D ) ) e. ( ( C Xc. D ) Func ( D FuncCat E ) ) )
30 eqid 
 |-  ( C 2ndF D ) = ( C 2ndF D )
31 20 26 2 30 2ndfcl 
 |-  ( ph -> ( C 2ndF D ) e. ( ( C Xc. D ) Func D ) )
32 22 23 29 31 prfcl 
 |-  ( ph -> ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) e. ( ( C Xc. D ) Func ( ( D FuncCat E ) Xc. D ) ) )
33 eqid 
 |-  ( D evalF E ) = ( D evalF E )
34 eqid 
 |-  ( D FuncCat E ) = ( D FuncCat E )
35 33 34 2 3 evlfcl 
 |-  ( ph -> ( D evalF E ) e. ( ( ( D FuncCat E ) Xc. D ) Func E ) )
36 7 8 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( A X. B ) )
37 11 12 opelxpd 
 |-  ( ph -> <. Z , W >. e. ( A X. B ) )
38 eqid 
 |-  ( Hom ` ( C Xc. D ) ) = ( Hom ` ( C Xc. D ) )
39 13 14 opelxpd 
 |-  ( ph -> <. R , S >. e. ( ( X H Z ) X. ( Y J W ) ) )
40 20 5 6 9 10 7 8 11 12 38 xpchom2 
 |-  ( ph -> ( <. X , Y >. ( Hom ` ( C Xc. D ) ) <. Z , W >. ) = ( ( X H Z ) X. ( Y J W ) ) )
41 39 40 eleqtrrd 
 |-  ( ph -> <. R , S >. e. ( <. X , Y >. ( Hom ` ( C Xc. D ) ) <. Z , W >. ) )
42 21 32 35 36 37 38 41 cofu2 
 |-  ( ph -> ( ( <. X , Y >. ( 2nd ` ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ) <. Z , W >. ) ` <. R , S >. ) = ( ( ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) ( 2nd ` ( D evalF E ) ) ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. Z , W >. ) ) ` ( ( <. X , Y >. ( 2nd ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) <. Z , W >. ) ` <. R , S >. ) ) )
43 19 42 syl5eq 
 |-  ( ph -> ( R ( <. X , Y >. ( 2nd ` ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ) <. Z , W >. ) S ) = ( ( ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) ( 2nd ` ( D evalF E ) ) ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. Z , W >. ) ) ` ( ( <. X , Y >. ( 2nd ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) <. Z , W >. ) ` <. R , S >. ) ) )
44 18 43 eqtrd 
 |-  ( ph -> ( R ( <. X , Y >. ( 2nd ` F ) <. Z , W >. ) S ) = ( ( ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) ( 2nd ` ( D evalF E ) ) ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. Z , W >. ) ) ` ( ( <. X , Y >. ( 2nd ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) <. Z , W >. ) ` <. R , S >. ) ) )
45 22 21 38 29 31 36 prf1 
 |-  ( ph -> ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) = <. ( ( 1st ` ( G o.func ( C 1stF D ) ) ) ` <. X , Y >. ) , ( ( 1st ` ( C 2ndF D ) ) ` <. X , Y >. ) >. )
46 21 28 4 36 cofu1 
 |-  ( ph -> ( ( 1st ` ( G o.func ( C 1stF D ) ) ) ` <. X , Y >. ) = ( ( 1st ` G ) ` ( ( 1st ` ( C 1stF D ) ) ` <. X , Y >. ) ) )
47 20 21 38 26 2 27 36 1stf1 
 |-  ( ph -> ( ( 1st ` ( C 1stF D ) ) ` <. X , Y >. ) = ( 1st ` <. X , Y >. ) )
48 op1stg 
 |-  ( ( X e. A /\ Y e. B ) -> ( 1st ` <. X , Y >. ) = X )
49 7 8 48 syl2anc 
 |-  ( ph -> ( 1st ` <. X , Y >. ) = X )
50 47 49 eqtrd 
 |-  ( ph -> ( ( 1st ` ( C 1stF D ) ) ` <. X , Y >. ) = X )
51 50 fveq2d 
 |-  ( ph -> ( ( 1st ` G ) ` ( ( 1st ` ( C 1stF D ) ) ` <. X , Y >. ) ) = ( ( 1st ` G ) ` X ) )
52 46 51 eqtrd 
 |-  ( ph -> ( ( 1st ` ( G o.func ( C 1stF D ) ) ) ` <. X , Y >. ) = ( ( 1st ` G ) ` X ) )
53 20 21 38 26 2 30 36 2ndf1 
 |-  ( ph -> ( ( 1st ` ( C 2ndF D ) ) ` <. X , Y >. ) = ( 2nd ` <. X , Y >. ) )
54 op2ndg 
 |-  ( ( X e. A /\ Y e. B ) -> ( 2nd ` <. X , Y >. ) = Y )
55 7 8 54 syl2anc 
 |-  ( ph -> ( 2nd ` <. X , Y >. ) = Y )
56 53 55 eqtrd 
 |-  ( ph -> ( ( 1st ` ( C 2ndF D ) ) ` <. X , Y >. ) = Y )
57 52 56 opeq12d 
 |-  ( ph -> <. ( ( 1st ` ( G o.func ( C 1stF D ) ) ) ` <. X , Y >. ) , ( ( 1st ` ( C 2ndF D ) ) ` <. X , Y >. ) >. = <. ( ( 1st ` G ) ` X ) , Y >. )
58 45 57 eqtrd 
 |-  ( ph -> ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) = <. ( ( 1st ` G ) ` X ) , Y >. )
59 22 21 38 29 31 37 prf1 
 |-  ( ph -> ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. Z , W >. ) = <. ( ( 1st ` ( G o.func ( C 1stF D ) ) ) ` <. Z , W >. ) , ( ( 1st ` ( C 2ndF D ) ) ` <. Z , W >. ) >. )
60 21 28 4 37 cofu1 
 |-  ( ph -> ( ( 1st ` ( G o.func ( C 1stF D ) ) ) ` <. Z , W >. ) = ( ( 1st ` G ) ` ( ( 1st ` ( C 1stF D ) ) ` <. Z , W >. ) ) )
61 20 21 38 26 2 27 37 1stf1 
 |-  ( ph -> ( ( 1st ` ( C 1stF D ) ) ` <. Z , W >. ) = ( 1st ` <. Z , W >. ) )
62 op1stg 
 |-  ( ( Z e. A /\ W e. B ) -> ( 1st ` <. Z , W >. ) = Z )
63 11 12 62 syl2anc 
 |-  ( ph -> ( 1st ` <. Z , W >. ) = Z )
64 61 63 eqtrd 
 |-  ( ph -> ( ( 1st ` ( C 1stF D ) ) ` <. Z , W >. ) = Z )
65 64 fveq2d 
 |-  ( ph -> ( ( 1st ` G ) ` ( ( 1st ` ( C 1stF D ) ) ` <. Z , W >. ) ) = ( ( 1st ` G ) ` Z ) )
66 60 65 eqtrd 
 |-  ( ph -> ( ( 1st ` ( G o.func ( C 1stF D ) ) ) ` <. Z , W >. ) = ( ( 1st ` G ) ` Z ) )
67 20 21 38 26 2 30 37 2ndf1 
 |-  ( ph -> ( ( 1st ` ( C 2ndF D ) ) ` <. Z , W >. ) = ( 2nd ` <. Z , W >. ) )
68 op2ndg 
 |-  ( ( Z e. A /\ W e. B ) -> ( 2nd ` <. Z , W >. ) = W )
69 11 12 68 syl2anc 
 |-  ( ph -> ( 2nd ` <. Z , W >. ) = W )
70 67 69 eqtrd 
 |-  ( ph -> ( ( 1st ` ( C 2ndF D ) ) ` <. Z , W >. ) = W )
71 66 70 opeq12d 
 |-  ( ph -> <. ( ( 1st ` ( G o.func ( C 1stF D ) ) ) ` <. Z , W >. ) , ( ( 1st ` ( C 2ndF D ) ) ` <. Z , W >. ) >. = <. ( ( 1st ` G ) ` Z ) , W >. )
72 59 71 eqtrd 
 |-  ( ph -> ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. Z , W >. ) = <. ( ( 1st ` G ) ` Z ) , W >. )
73 58 72 oveq12d 
 |-  ( ph -> ( ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) ( 2nd ` ( D evalF E ) ) ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. Z , W >. ) ) = ( <. ( ( 1st ` G ) ` X ) , Y >. ( 2nd ` ( D evalF E ) ) <. ( ( 1st ` G ) ` Z ) , W >. ) )
74 22 21 38 29 31 36 37 41 prf2 
 |-  ( ph -> ( ( <. X , Y >. ( 2nd ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) <. Z , W >. ) ` <. R , S >. ) = <. ( ( <. X , Y >. ( 2nd ` ( G o.func ( C 1stF D ) ) ) <. Z , W >. ) ` <. R , S >. ) , ( ( <. X , Y >. ( 2nd ` ( C 2ndF D ) ) <. Z , W >. ) ` <. R , S >. ) >. )
75 21 28 4 36 37 38 41 cofu2 
 |-  ( ph -> ( ( <. X , Y >. ( 2nd ` ( G o.func ( C 1stF D ) ) ) <. Z , W >. ) ` <. R , S >. ) = ( ( ( ( 1st ` ( C 1stF D ) ) ` <. X , Y >. ) ( 2nd ` G ) ( ( 1st ` ( C 1stF D ) ) ` <. Z , W >. ) ) ` ( ( <. X , Y >. ( 2nd ` ( C 1stF D ) ) <. Z , W >. ) ` <. R , S >. ) ) )
76 50 64 oveq12d 
 |-  ( ph -> ( ( ( 1st ` ( C 1stF D ) ) ` <. X , Y >. ) ( 2nd ` G ) ( ( 1st ` ( C 1stF D ) ) ` <. Z , W >. ) ) = ( X ( 2nd ` G ) Z ) )
77 20 21 38 26 2 27 36 37 1stf2 
 |-  ( ph -> ( <. X , Y >. ( 2nd ` ( C 1stF D ) ) <. Z , W >. ) = ( 1st |` ( <. X , Y >. ( Hom ` ( C Xc. D ) ) <. Z , W >. ) ) )
78 77 fveq1d 
 |-  ( ph -> ( ( <. X , Y >. ( 2nd ` ( C 1stF D ) ) <. Z , W >. ) ` <. R , S >. ) = ( ( 1st |` ( <. X , Y >. ( Hom ` ( C Xc. D ) ) <. Z , W >. ) ) ` <. R , S >. ) )
79 41 fvresd 
 |-  ( ph -> ( ( 1st |` ( <. X , Y >. ( Hom ` ( C Xc. D ) ) <. Z , W >. ) ) ` <. R , S >. ) = ( 1st ` <. R , S >. ) )
80 op1stg 
 |-  ( ( R e. ( X H Z ) /\ S e. ( Y J W ) ) -> ( 1st ` <. R , S >. ) = R )
81 13 14 80 syl2anc 
 |-  ( ph -> ( 1st ` <. R , S >. ) = R )
82 78 79 81 3eqtrd 
 |-  ( ph -> ( ( <. X , Y >. ( 2nd ` ( C 1stF D ) ) <. Z , W >. ) ` <. R , S >. ) = R )
83 76 82 fveq12d 
 |-  ( ph -> ( ( ( ( 1st ` ( C 1stF D ) ) ` <. X , Y >. ) ( 2nd ` G ) ( ( 1st ` ( C 1stF D ) ) ` <. Z , W >. ) ) ` ( ( <. X , Y >. ( 2nd ` ( C 1stF D ) ) <. Z , W >. ) ` <. R , S >. ) ) = ( ( X ( 2nd ` G ) Z ) ` R ) )
84 75 83 eqtrd 
 |-  ( ph -> ( ( <. X , Y >. ( 2nd ` ( G o.func ( C 1stF D ) ) ) <. Z , W >. ) ` <. R , S >. ) = ( ( X ( 2nd ` G ) Z ) ` R ) )
85 20 21 38 26 2 30 36 37 2ndf2 
 |-  ( ph -> ( <. X , Y >. ( 2nd ` ( C 2ndF D ) ) <. Z , W >. ) = ( 2nd |` ( <. X , Y >. ( Hom ` ( C Xc. D ) ) <. Z , W >. ) ) )
86 85 fveq1d 
 |-  ( ph -> ( ( <. X , Y >. ( 2nd ` ( C 2ndF D ) ) <. Z , W >. ) ` <. R , S >. ) = ( ( 2nd |` ( <. X , Y >. ( Hom ` ( C Xc. D ) ) <. Z , W >. ) ) ` <. R , S >. ) )
87 41 fvresd 
 |-  ( ph -> ( ( 2nd |` ( <. X , Y >. ( Hom ` ( C Xc. D ) ) <. Z , W >. ) ) ` <. R , S >. ) = ( 2nd ` <. R , S >. ) )
88 op2ndg 
 |-  ( ( R e. ( X H Z ) /\ S e. ( Y J W ) ) -> ( 2nd ` <. R , S >. ) = S )
89 13 14 88 syl2anc 
 |-  ( ph -> ( 2nd ` <. R , S >. ) = S )
90 86 87 89 3eqtrd 
 |-  ( ph -> ( ( <. X , Y >. ( 2nd ` ( C 2ndF D ) ) <. Z , W >. ) ` <. R , S >. ) = S )
91 84 90 opeq12d 
 |-  ( ph -> <. ( ( <. X , Y >. ( 2nd ` ( G o.func ( C 1stF D ) ) ) <. Z , W >. ) ` <. R , S >. ) , ( ( <. X , Y >. ( 2nd ` ( C 2ndF D ) ) <. Z , W >. ) ` <. R , S >. ) >. = <. ( ( X ( 2nd ` G ) Z ) ` R ) , S >. )
92 74 91 eqtrd 
 |-  ( ph -> ( ( <. X , Y >. ( 2nd ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) <. Z , W >. ) ` <. R , S >. ) = <. ( ( X ( 2nd ` G ) Z ) ` R ) , S >. )
93 73 92 fveq12d 
 |-  ( ph -> ( ( ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) ( 2nd ` ( D evalF E ) ) ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. Z , W >. ) ) ` ( ( <. X , Y >. ( 2nd ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) <. Z , W >. ) ` <. R , S >. ) ) = ( ( <. ( ( 1st ` G ) ` X ) , Y >. ( 2nd ` ( D evalF E ) ) <. ( ( 1st ` G ) ` Z ) , W >. ) ` <. ( ( X ( 2nd ` G ) Z ) ` R ) , S >. ) )
94 df-ov 
 |-  ( ( ( X ( 2nd ` G ) Z ) ` R ) ( <. ( ( 1st ` G ) ` X ) , Y >. ( 2nd ` ( D evalF E ) ) <. ( ( 1st ` G ) ` Z ) , W >. ) S ) = ( ( <. ( ( 1st ` G ) ` X ) , Y >. ( 2nd ` ( D evalF E ) ) <. ( ( 1st ` G ) ` Z ) , W >. ) ` <. ( ( X ( 2nd ` G ) Z ) ` R ) , S >. )
95 93 94 eqtr4di 
 |-  ( ph -> ( ( ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. X , Y >. ) ( 2nd ` ( D evalF E ) ) ( ( 1st ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) ` <. Z , W >. ) ) ` ( ( <. X , Y >. ( 2nd ` ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) <. Z , W >. ) ` <. R , S >. ) ) = ( ( ( X ( 2nd ` G ) Z ) ` R ) ( <. ( ( 1st ` G ) ` X ) , Y >. ( 2nd ` ( D evalF E ) ) <. ( ( 1st ` G ) ` Z ) , W >. ) S ) )
96 eqid 
 |-  ( comp ` E ) = ( comp ` E )
97 eqid 
 |-  ( D Nat E ) = ( D Nat E )
98 34 fucbas 
 |-  ( D Func E ) = ( Base ` ( D FuncCat E ) )
99 relfunc 
 |-  Rel ( C Func ( D FuncCat E ) )
100 1st2ndbr 
 |-  ( ( Rel ( C Func ( D FuncCat E ) ) /\ G e. ( C Func ( D FuncCat E ) ) ) -> ( 1st ` G ) ( C Func ( D FuncCat E ) ) ( 2nd ` G ) )
101 99 4 100 sylancr 
 |-  ( ph -> ( 1st ` G ) ( C Func ( D FuncCat E ) ) ( 2nd ` G ) )
102 5 98 101 funcf1 
 |-  ( ph -> ( 1st ` G ) : A --> ( D Func E ) )
103 102 7 ffvelrnd 
 |-  ( ph -> ( ( 1st ` G ) ` X ) e. ( D Func E ) )
104 102 11 ffvelrnd 
 |-  ( ph -> ( ( 1st ` G ) ` Z ) e. ( D Func E ) )
105 eqid 
 |-  ( <. ( ( 1st ` G ) ` X ) , Y >. ( 2nd ` ( D evalF E ) ) <. ( ( 1st ` G ) ` Z ) , W >. ) = ( <. ( ( 1st ` G ) ` X ) , Y >. ( 2nd ` ( D evalF E ) ) <. ( ( 1st ` G ) ` Z ) , W >. )
106 34 97 fuchom 
 |-  ( D Nat E ) = ( Hom ` ( D FuncCat E ) )
107 5 9 106 101 7 11 funcf2 
 |-  ( ph -> ( X ( 2nd ` G ) Z ) : ( X H Z ) --> ( ( ( 1st ` G ) ` X ) ( D Nat E ) ( ( 1st ` G ) ` Z ) ) )
108 107 13 ffvelrnd 
 |-  ( ph -> ( ( X ( 2nd ` G ) Z ) ` R ) e. ( ( ( 1st ` G ) ` X ) ( D Nat E ) ( ( 1st ` G ) ` Z ) ) )
109 33 2 3 6 10 96 97 103 104 8 12 105 108 14 evlf2val 
 |-  ( ph -> ( ( ( X ( 2nd ` G ) Z ) ` R ) ( <. ( ( 1st ` G ) ` X ) , Y >. ( 2nd ` ( D evalF E ) ) <. ( ( 1st ` G ) ` Z ) , W >. ) S ) = ( ( ( ( X ( 2nd ` G ) Z ) ` R ) ` W ) ( <. ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` Y ) , ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` W ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` Z ) ) ` W ) ) ( ( Y ( 2nd ` ( ( 1st ` G ) ` X ) ) W ) ` S ) ) )
110 44 95 109 3eqtrd 
 |-  ( ph -> ( R ( <. X , Y >. ( 2nd ` F ) <. Z , W >. ) S ) = ( ( ( ( X ( 2nd ` G ) Z ) ` R ) ` W ) ( <. ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` Y ) , ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` W ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` Z ) ) ` W ) ) ( ( Y ( 2nd ` ( ( 1st ` G ) ` X ) ) W ) ` S ) ) )