Metamath Proof Explorer


Theorem uncfcurf

Description: Cancellation of uncurry with curry. (Contributed by Mario Carneiro, 13-Jan-2017)

Ref Expression
Hypotheses uncfcurf.g G = C D curry F F
uncfcurf.c φ C Cat
uncfcurf.d φ D Cat
uncfcurf.f φ F C × c D Func E
Assertion uncfcurf φ ⟨“ CDE ”⟩ uncurry F G = F

Proof

Step Hyp Ref Expression
1 uncfcurf.g G = C D curry F F
2 uncfcurf.c φ C Cat
3 uncfcurf.d φ D Cat
4 uncfcurf.f φ F C × c D Func E
5 eqid ⟨“ CDE ”⟩ uncurry F G = ⟨“ CDE ”⟩ uncurry F G
6 3 adantr φ x Base C y Base D D Cat
7 funcrcl F C × c D Func E C × c D Cat E Cat
8 4 7 syl φ C × c D Cat E Cat
9 8 simprd φ E Cat
10 9 adantr φ x Base C y Base D E Cat
11 eqid D FuncCat E = D FuncCat E
12 1 11 2 3 4 curfcl φ G C Func D FuncCat E
13 12 adantr φ x Base C y Base D G C Func D FuncCat E
14 eqid Base C = Base C
15 eqid Base D = Base D
16 simprl φ x Base C y Base D x Base C
17 simprr φ x Base C y Base D y Base D
18 5 6 10 13 14 15 16 17 uncf1 φ x Base C y Base D x 1 st ⟨“ CDE ”⟩ uncurry F G y = 1 st 1 st G x y
19 2 adantr φ x Base C y Base D C Cat
20 4 adantr φ x Base C y Base D F C × c D Func E
21 eqid 1 st G x = 1 st G x
22 1 14 19 6 20 15 16 21 17 curf11 φ x Base C y Base D 1 st 1 st G x y = x 1 st F y
23 18 22 eqtrd φ x Base C y Base D x 1 st ⟨“ CDE ”⟩ uncurry F G y = x 1 st F y
24 23 ralrimivva φ x Base C y Base D x 1 st ⟨“ CDE ”⟩ uncurry F G y = x 1 st F y
25 eqid C × c D = C × c D
26 25 14 15 xpcbas Base C × Base D = Base C × c D
27 eqid Base E = Base E
28 relfunc Rel C × c D Func E
29 5 3 9 12 uncfcl φ ⟨“ CDE ”⟩ uncurry F G C × c D Func E
30 1st2ndbr Rel C × c D Func E ⟨“ CDE ”⟩ uncurry F G C × c D Func E 1 st ⟨“ CDE ”⟩ uncurry F G C × c D Func E 2 nd ⟨“ CDE ”⟩ uncurry F G
31 28 29 30 sylancr φ 1 st ⟨“ CDE ”⟩ uncurry F G C × c D Func E 2 nd ⟨“ CDE ”⟩ uncurry F G
32 26 27 31 funcf1 φ 1 st ⟨“ CDE ”⟩ uncurry F G : Base C × Base D Base E
33 32 ffnd φ 1 st ⟨“ CDE ”⟩ uncurry F G Fn Base C × Base D
34 1st2ndbr Rel C × c D Func E F C × c D Func E 1 st F C × c D Func E 2 nd F
35 28 4 34 sylancr φ 1 st F C × c D Func E 2 nd F
36 26 27 35 funcf1 φ 1 st F : Base C × Base D Base E
37 36 ffnd φ 1 st F Fn Base C × Base D
38 eqfnov2 1 st ⟨“ CDE ”⟩ uncurry F G Fn Base C × Base D 1 st F Fn Base C × Base D 1 st ⟨“ CDE ”⟩ uncurry F G = 1 st F x Base C y Base D x 1 st ⟨“ CDE ”⟩ uncurry F G y = x 1 st F y
39 33 37 38 syl2anc φ 1 st ⟨“ CDE ”⟩ uncurry F G = 1 st F x Base C y Base D x 1 st ⟨“ CDE ”⟩ uncurry F G y = x 1 st F y
40 24 39 mpbird φ 1 st ⟨“ CDE ”⟩ uncurry F G = 1 st F
41 3 ad3antrrr φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w D Cat
42 9 ad3antrrr φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w E Cat
43 12 ad3antrrr φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w G C Func D FuncCat E
44 16 adantr φ x Base C y Base D z Base C w Base D x Base C
45 44 adantr φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w x Base C
46 17 adantr φ x Base C y Base D z Base C w Base D y Base D
47 46 adantr φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w y Base D
48 eqid Hom C = Hom C
49 eqid Hom D = Hom D
50 simprl φ x Base C y Base D z Base C w Base D z Base C
51 50 adantr φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w z Base C
52 simprr φ x Base C y Base D z Base C w Base D w Base D
53 52 adantr φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w w Base D
54 simprl φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w f x Hom C z
55 simprr φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w g y Hom D w
56 5 41 42 43 14 15 45 47 48 49 51 53 54 55 uncf2 φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w f x y 2 nd ⟨“ CDE ”⟩ uncurry F G z w g = x 2 nd G z f 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 g
57 2 ad3antrrr φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w C Cat
58 4 ad3antrrr φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w F C × c D Func E
59 1 14 57 41 58 15 45 21 47 curf11 φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w 1 st 1 st G x y = x 1 st F y
60 df-ov x 1 st F y = 1 st F x y
61 59 60 syl6eq φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w 1 st 1 st G x y = 1 st F x y
62 1 14 57 41 58 15 45 21 53 curf11 φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w 1 st 1 st G x w = x 1 st F w
63 df-ov x 1 st F w = 1 st F x w
64 62 63 syl6eq φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w 1 st 1 st G x w = 1 st F x w
65 61 64 opeq12d φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w 1 st 1 st G x y 1 st 1 st G x w = 1 st F x y 1 st F x w
66 eqid 1 st G z = 1 st G z
67 1 14 57 41 58 15 51 66 53 curf11 φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w 1 st 1 st G z w = z 1 st F w
68 df-ov z 1 st F w = 1 st F z w
69 67 68 syl6eq φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w 1 st 1 st G z w = 1 st F z w
70 65 69 oveq12d φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w 1 st 1 st G x y 1 st 1 st G x w comp E 1 st 1 st G z w = 1 st F x y 1 st F x w comp E 1 st F z w
71 eqid Id D = Id D
72 eqid x 2 nd G z f = x 2 nd G z f
73 1 14 57 41 58 15 48 71 45 51 54 72 53 curf2val φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w x 2 nd G z f w = f x w 2 nd F z w Id D w
74 df-ov f x w 2 nd F z w Id D w = x w 2 nd F z w f Id D w
75 73 74 syl6eq φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w x 2 nd G z f w = x w 2 nd F z w f Id D w
76 eqid Id C = Id C
77 1 14 57 41 58 15 45 21 47 49 76 53 55 curf12 φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w y 2 nd 1 st G x w g = Id C x x y 2 nd F x w g
78 df-ov Id C x x y 2 nd F x w g = x y 2 nd F x w Id C x g
79 77 78 syl6eq φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w y 2 nd 1 st G x w g = x y 2 nd F x w Id C x g
80 70 75 79 oveq123d φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w x 2 nd G z f 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 g = x w 2 nd F z w f Id D w 1 st F x y 1 st F x w comp E 1 st F z w x y 2 nd F x w Id C x g
81 eqid Hom C × c D = Hom C × c D
82 eqid comp C × c D = comp C × c D
83 eqid comp E = comp E
84 35 ad2antrr φ x Base C y Base D z Base C w Base D 1 st F C × c D Func E 2 nd F
85 84 adantr φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w 1 st F C × c D Func E 2 nd F
86 opelxpi x Base C y Base D x y Base C × Base D
87 86 ad2antlr φ x Base C y Base D z Base C w Base D x y Base C × Base D
88 87 adantr φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w x y Base C × Base D
89 45 53 opelxpd φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w x w Base C × Base D
90 opelxpi z Base C w Base D z w Base C × Base D
91 90 adantl φ x Base C y Base D z Base C w Base D z w Base C × Base D
92 91 adantr φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w z w Base C × Base D
93 14 48 76 57 45 catidcl φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w Id C x x Hom C x
94 93 55 opelxpd φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w Id C x g x Hom C x × y Hom D w
95 25 14 15 48 49 45 47 45 53 81 xpchom2 φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w x y Hom C × c D x w = x Hom C x × y Hom D w
96 94 95 eleqtrrd φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w Id C x g x y Hom C × c D x w
97 15 49 71 41 53 catidcl φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w Id D w w Hom D w
98 54 97 opelxpd φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w f Id D w x Hom C z × w Hom D w
99 25 14 15 48 49 45 53 51 53 81 xpchom2 φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w x w Hom C × c D z w = x Hom C z × w Hom D w
100 98 99 eleqtrrd φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w f Id D w x w Hom C × c D z w
101 26 81 82 83 85 88 89 92 96 100 funcco φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w x y 2 nd F z w f Id D w x y x w comp C × c D z w Id C x g = x w 2 nd F z w f Id D w 1 st F x y 1 st F x w comp E 1 st F z w x y 2 nd F x w Id C x g
102 eqid comp C = comp C
103 eqid comp D = comp D
104 25 14 15 48 49 45 47 45 53 102 103 82 51 53 93 55 54 97 xpcco2 φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w f Id D w x y x w comp C × c D z w Id C x g = f x x comp C z Id C x Id D w y w comp D w g
105 104 fveq2d φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w x y 2 nd F z w f Id D w x y x w comp C × c D z w Id C x g = x y 2 nd F z w f x x comp C z Id C x Id D w y w comp D w g
106 df-ov f x x comp C z Id C x x y 2 nd F z w Id D w y w comp D w g = x y 2 nd F z w f x x comp C z Id C x Id D w y w comp D w g
107 105 106 syl6eqr φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w x y 2 nd F z w f Id D w x y x w comp C × c D z w Id C x g = f x x comp C z Id C x x y 2 nd F z w Id D w y w comp D w g
108 14 48 76 57 45 102 51 54 catrid φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w f x x comp C z Id C x = f
109 15 49 71 41 47 103 53 55 catlid φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w Id D w y w comp D w g = g
110 108 109 oveq12d φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w f x x comp C z Id C x x y 2 nd F z w Id D w y w comp D w g = f x y 2 nd F z w g
111 107 110 eqtrd φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w x y 2 nd F z w f Id D w x y x w comp C × c D z w Id C x g = f x y 2 nd F z w g
112 80 101 111 3eqtr2d φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w x 2 nd G z f 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 g = f x y 2 nd F z w g
113 56 112 eqtrd φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w f x y 2 nd ⟨“ CDE ”⟩ uncurry F G z w g = f x y 2 nd F z w g
114 113 ralrimivva φ x Base C y Base D z Base C w Base D f x Hom C z g y Hom D w f x y 2 nd ⟨“ CDE ”⟩ uncurry F G z w g = f x y 2 nd F z w g
115 eqid Hom E = Hom E
116 31 ad2antrr φ x Base C y Base D z Base C w Base D 1 st ⟨“ CDE ”⟩ uncurry F G C × c D Func E 2 nd ⟨“ CDE ”⟩ uncurry F G
117 26 81 115 116 87 91 funcf2 φ x Base C y Base D z Base C w Base D x y 2 nd ⟨“ CDE ”⟩ uncurry F G z w : x y Hom C × c D z w 1 st ⟨“ CDE ”⟩ uncurry F G x y Hom E 1 st ⟨“ CDE ”⟩ uncurry F G z w
118 25 14 15 48 49 44 46 50 52 81 xpchom2 φ x Base C y Base D z Base C w Base D x y Hom C × c D z w = x Hom C z × y Hom D w
119 118 feq2d φ x Base C y Base D z Base C w Base D x y 2 nd ⟨“ CDE ”⟩ uncurry F G z w : x y Hom C × c D z w 1 st ⟨“ CDE ”⟩ uncurry F G x y Hom E 1 st ⟨“ CDE ”⟩ uncurry F G z w x y 2 nd ⟨“ CDE ”⟩ uncurry F G z w : x Hom C z × y Hom D w 1 st ⟨“ CDE ”⟩ uncurry F G x y Hom E 1 st ⟨“ CDE ”⟩ uncurry F G z w
120 117 119 mpbid φ x Base C y Base D z Base C w Base D x y 2 nd ⟨“ CDE ”⟩ uncurry F G z w : x Hom C z × y Hom D w 1 st ⟨“ CDE ”⟩ uncurry F G x y Hom E 1 st ⟨“ CDE ”⟩ uncurry F G z w
121 120 ffnd φ x Base C y Base D z Base C w Base D x y 2 nd ⟨“ CDE ”⟩ uncurry F G z w Fn x Hom C z × y Hom D w
122 26 81 115 84 87 91 funcf2 φ x Base C y Base D z Base C w Base D x y 2 nd F z w : x y Hom C × c D z w 1 st F x y Hom E 1 st F z w
123 118 feq2d φ x Base C y Base D z Base C w Base D x y 2 nd F z w : x y Hom C × c D z w 1 st F x y Hom E 1 st F z w x y 2 nd F z w : x Hom C z × y Hom D w 1 st F x y Hom E 1 st F z w
124 122 123 mpbid φ x Base C y Base D z Base C w Base D x y 2 nd F z w : x Hom C z × y Hom D w 1 st F x y Hom E 1 st F z w
125 124 ffnd φ x Base C y Base D z Base C w Base D x y 2 nd F z w Fn x Hom C z × y Hom D w
126 eqfnov2 x y 2 nd ⟨“ CDE ”⟩ uncurry F G z w Fn x Hom C z × y Hom D w x y 2 nd F z w Fn x Hom C z × y Hom D w x y 2 nd ⟨“ CDE ”⟩ uncurry F G z w = x y 2 nd F z w f x Hom C z g y Hom D w f x y 2 nd ⟨“ CDE ”⟩ uncurry F G z w g = f x y 2 nd F z w g
127 121 125 126 syl2anc φ x Base C y Base D z Base C w Base D x y 2 nd ⟨“ CDE ”⟩ uncurry F G z w = x y 2 nd F z w f x Hom C z g y Hom D w f x y 2 nd ⟨“ CDE ”⟩ uncurry F G z w g = f x y 2 nd F z w g
128 114 127 mpbird φ x Base C y Base D z Base C w Base D x y 2 nd ⟨“ CDE ”⟩ uncurry F G z w = x y 2 nd F z w
129 128 ralrimivva φ x Base C y Base D z Base C w Base D x y 2 nd ⟨“ CDE ”⟩ uncurry F G z w = x y 2 nd F z w
130 129 ralrimivva φ x Base C y Base D z Base C w Base D x y 2 nd ⟨“ CDE ”⟩ uncurry F G z w = x y 2 nd F z w
131 oveq2 v = z w u 2 nd ⟨“ CDE ”⟩ uncurry F G v = u 2 nd ⟨“ CDE ”⟩ uncurry F G z w
132 oveq2 v = z w u 2 nd F v = u 2 nd F z w
133 131 132 eqeq12d v = z w u 2 nd ⟨“ CDE ”⟩ uncurry F G v = u 2 nd F v u 2 nd ⟨“ CDE ”⟩ uncurry F G z w = u 2 nd F z w
134 133 ralxp v Base C × Base D u 2 nd ⟨“ CDE ”⟩ uncurry F G v = u 2 nd F v z Base C w Base D u 2 nd ⟨“ CDE ”⟩ uncurry F G z w = u 2 nd F z w
135 oveq1 u = x y u 2 nd ⟨“ CDE ”⟩ uncurry F G z w = x y 2 nd ⟨“ CDE ”⟩ uncurry F G z w
136 oveq1 u = x y u 2 nd F z w = x y 2 nd F z w
137 135 136 eqeq12d u = x y u 2 nd ⟨“ CDE ”⟩ uncurry F G z w = u 2 nd F z w x y 2 nd ⟨“ CDE ”⟩ uncurry F G z w = x y 2 nd F z w
138 137 2ralbidv u = x y z Base C w Base D u 2 nd ⟨“ CDE ”⟩ uncurry F G z w = u 2 nd F z w z Base C w Base D x y 2 nd ⟨“ CDE ”⟩ uncurry F G z w = x y 2 nd F z w
139 134 138 syl5bb u = x y v Base C × Base D u 2 nd ⟨“ CDE ”⟩ uncurry F G v = u 2 nd F v z Base C w Base D x y 2 nd ⟨“ CDE ”⟩ uncurry F G z w = x y 2 nd F z w
140 139 ralxp u Base C × Base D v Base C × Base D u 2 nd ⟨“ CDE ”⟩ uncurry F G v = u 2 nd F v x Base C y Base D z Base C w Base D x y 2 nd ⟨“ CDE ”⟩ uncurry F G z w = x y 2 nd F z w
141 130 140 sylibr φ u Base C × Base D v Base C × Base D u 2 nd ⟨“ CDE ”⟩ uncurry F G v = u 2 nd F v
142 26 31 funcfn2 φ 2 nd ⟨“ CDE ”⟩ uncurry F G Fn Base C × Base D × Base C × Base D
143 26 35 funcfn2 φ 2 nd F Fn Base C × Base D × Base C × Base D
144 eqfnov2 2 nd ⟨“ CDE ”⟩ uncurry F G Fn Base C × Base D × Base C × Base D 2 nd F Fn Base C × Base D × Base C × Base D 2 nd ⟨“ CDE ”⟩ uncurry F G = 2 nd F u Base C × Base D v Base C × Base D u 2 nd ⟨“ CDE ”⟩ uncurry F G v = u 2 nd F v
145 142 143 144 syl2anc φ 2 nd ⟨“ CDE ”⟩ uncurry F G = 2 nd F u Base C × Base D v Base C × Base D u 2 nd ⟨“ CDE ”⟩ uncurry F G v = u 2 nd F v
146 141 145 mpbird φ 2 nd ⟨“ CDE ”⟩ uncurry F G = 2 nd F
147 40 146 opeq12d φ 1 st ⟨“ CDE ”⟩ uncurry F G 2 nd ⟨“ CDE ”⟩ uncurry F G = 1 st F 2 nd F
148 1st2nd Rel C × c D Func E ⟨“ CDE ”⟩ uncurry F G C × c D Func E ⟨“ CDE ”⟩ uncurry F G = 1 st ⟨“ CDE ”⟩ uncurry F G 2 nd ⟨“ CDE ”⟩ uncurry F G
149 28 29 148 sylancr φ ⟨“ CDE ”⟩ uncurry F G = 1 st ⟨“ CDE ”⟩ uncurry F G 2 nd ⟨“ CDE ”⟩ uncurry F G
150 1st2nd Rel C × c D Func E F C × c D Func E F = 1 st F 2 nd F
151 28 4 150 sylancr φ F = 1 st F 2 nd F
152 147 149 151 3eqtr4d φ ⟨“ CDE ”⟩ uncurry F G = F