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 = ⟨“ CDE ”⟩ uncurry F G
uncfval.c φ D Cat
uncfval.d φ E Cat
uncfval.f φ G C Func D FuncCat E
uncf1.a A = Base C
uncf1.b B = Base D
uncf1.x φ X A
uncf1.y φ Y B
uncf2.h H = Hom C
uncf2.j J = Hom D
uncf2.z φ Z A
uncf2.w φ W B
uncf2.r φ R X H Z
uncf2.s φ S Y J W
Assertion uncf2 φ R X Y 2 nd F Z W S = X 2 nd G Z R W 1 st 1 st G X Y 1 st 1 st G X W comp E 1 st 1 st G Z W Y 2 nd 1 st G X W S

Proof

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