Metamath Proof Explorer


Theorem iscatd2

Description: Version of iscatd with a uniform assumption list, for increased proof sharing capabilities. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses iscatd2.b φ B = Base C
iscatd2.h φ H = Hom C
iscatd2.o φ · ˙ = comp C
iscatd2.c φ C V
iscatd2.ps ψ x B y B z B w B f x H y g y H z k z H w
iscatd2.1 φ y B 1 ˙ y H y
iscatd2.2 φ ψ 1 ˙ x y · ˙ y f = f
iscatd2.3 φ ψ g y y · ˙ z 1 ˙ = g
iscatd2.4 φ ψ g x y · ˙ z f x H z
iscatd2.5 φ ψ k y z · ˙ w g x y · ˙ w f = k x z · ˙ w g x y · ˙ z f
Assertion iscatd2 φ C Cat Id C = y B 1 ˙

Proof

Step Hyp Ref Expression
1 iscatd2.b φ B = Base C
2 iscatd2.h φ H = Hom C
3 iscatd2.o φ · ˙ = comp C
4 iscatd2.c φ C V
5 iscatd2.ps ψ x B y B z B w B f x H y g y H z k z H w
6 iscatd2.1 φ y B 1 ˙ y H y
7 iscatd2.2 φ ψ 1 ˙ x y · ˙ y f = f
8 iscatd2.3 φ ψ g y y · ˙ z 1 ˙ = g
9 iscatd2.4 φ ψ g x y · ˙ z f x H z
10 iscatd2.5 φ ψ k y z · ˙ w g x y · ˙ w f = k x z · ˙ w g x y · ˙ z f
11 6 ne0d φ y B y H y
12 11 3ad2antr1 φ y B a B r a H y y H y
13 n0 y H y g g y H y
14 12 13 sylib φ y B a B r a H y g g y H y
15 n0 y H y k k y H y
16 12 15 sylib φ y B a B r a H y k k y H y
17 exdistrv g k g y H y k y H y g g y H y k k y H y
18 simpll φ y B a B r a H y g y H y k y H y φ
19 simplr2 φ y B a B r a H y g y H y k y H y a B
20 simplr1 φ y B a B r a H y g y H y k y H y y B
21 19 20 jca φ y B a B r a H y g y H y k y H y a B y B
22 simplr3 φ y B a B r a H y g y H y k y H y r a H y
23 simprl φ y B a B r a H y g y H y k y H y g y H y
24 simprr φ y B a B r a H y g y H y k y H y k y H y
25 22 23 24 3jca φ y B a B r a H y g y H y k y H y r a H y g y H y k y H y
26 simplll x = a z = y w = y f = r x = a
27 26 eleq1d x = a z = y w = y f = r x B a B
28 27 anbi1d x = a z = y w = y f = r x B y B a B y B
29 simpllr x = a z = y w = y f = r z = y
30 29 eleq1d x = a z = y w = y f = r z B y B
31 simplr x = a z = y w = y f = r w = y
32 31 eleq1d x = a z = y w = y f = r w B y B
33 30 32 anbi12d x = a z = y w = y f = r z B w B y B y B
34 anidm y B y B y B
35 33 34 bitrdi x = a z = y w = y f = r z B w B y B
36 simpr x = a z = y w = y f = r f = r
37 26 oveq1d x = a z = y w = y f = r x H y = a H y
38 36 37 eleq12d x = a z = y w = y f = r f x H y r a H y
39 29 oveq2d x = a z = y w = y f = r y H z = y H y
40 39 eleq2d x = a z = y w = y f = r g y H z g y H y
41 29 31 oveq12d x = a z = y w = y f = r z H w = y H y
42 41 eleq2d x = a z = y w = y f = r k z H w k y H y
43 38 40 42 3anbi123d x = a z = y w = y f = r f x H y g y H z k z H w r a H y g y H y k y H y
44 28 35 43 3anbi123d x = a z = y w = y f = r x B y B z B w B f x H y g y H z k z H w a B y B y B r a H y g y H y k y H y
45 5 44 syl5bb x = a z = y w = y f = r ψ a B y B y B r a H y g y H y k y H y
46 45 anbi2d x = a z = y w = y f = r φ ψ φ a B y B y B r a H y g y H y k y H y
47 26 opeq1d x = a z = y w = y f = r x y = a y
48 47 oveq1d x = a z = y w = y f = r x y · ˙ y = a y · ˙ y
49 eqidd x = a z = y w = y f = r 1 ˙ = 1 ˙
50 48 49 36 oveq123d x = a z = y w = y f = r 1 ˙ x y · ˙ y f = 1 ˙ a y · ˙ y r
51 50 36 eqeq12d x = a z = y w = y f = r 1 ˙ x y · ˙ y f = f 1 ˙ a y · ˙ y r = r
52 46 51 imbi12d x = a z = y w = y f = r φ ψ 1 ˙ x y · ˙ y f = f φ a B y B y B r a H y g y H y k y H y 1 ˙ a y · ˙ y r = r
53 52 sbiedvw x = a z = y w = y r f φ ψ 1 ˙ x y · ˙ y f = f φ a B y B y B r a H y g y H y k y H y 1 ˙ a y · ˙ y r = r
54 53 sbiedvw x = a z = y y w r f φ ψ 1 ˙ x y · ˙ y f = f φ a B y B y B r a H y g y H y k y H y 1 ˙ a y · ˙ y r = r
55 54 sbiedvw x = a y z y w r f φ ψ 1 ˙ x y · ˙ y f = f φ a B y B y B r a H y g y H y k y H y 1 ˙ a y · ˙ y r = r
56 7 sbt r f φ ψ 1 ˙ x y · ˙ y f = f
57 56 sbt y w r f φ ψ 1 ˙ x y · ˙ y f = f
58 57 sbt y z y w r f φ ψ 1 ˙ x y · ˙ y f = f
59 55 58 chvarvv φ a B y B y B r a H y g y H y k y H y 1 ˙ a y · ˙ y r = r
60 18 21 20 25 59 syl13anc φ y B a B r a H y g y H y k y H y 1 ˙ a y · ˙ y r = r
61 60 ex φ y B a B r a H y g y H y k y H y 1 ˙ a y · ˙ y r = r
62 61 exlimdvv φ y B a B r a H y g k g y H y k y H y 1 ˙ a y · ˙ y r = r
63 17 62 syl5bir φ y B a B r a H y g g y H y k k y H y 1 ˙ a y · ˙ y r = r
64 14 16 63 mp2and φ y B a B r a H y 1 ˙ a y · ˙ y r = r
65 11 3ad2antr1 φ y B a B r y H a y H y
66 n0 y H y f f y H y
67 65 66 sylib φ y B a B r y H a f f y H y
68 id y = a y = a
69 68 68 oveq12d y = a y H y = a H a
70 69 neeq1d y = a y H y a H a
71 11 ralrimiva φ y B y H y
72 71 adantr φ y B a B r y H a y B y H y
73 simpr2 φ y B a B r y H a a B
74 70 72 73 rspcdva φ y B a B r y H a a H a
75 n0 a H a k k a H a
76 74 75 sylib φ y B a B r y H a k k a H a
77 exdistrv f k f y H y k a H a f f y H y k k a H a
78 simpll φ y B a B r y H a f y H y k a H a φ
79 simplr1 φ y B a B r y H a f y H y k a H a y B
80 simplr2 φ y B a B r y H a f y H y k a H a a B
81 simprl φ y B a B r y H a f y H y k a H a f y H y
82 simplr3 φ y B a B r y H a f y H y k a H a r y H a
83 simprr φ y B a B r y H a f y H y k a H a k a H a
84 81 82 83 3jca φ y B a B r y H a f y H y k a H a f y H y r y H a k a H a
85 simplll x = y z = a w = a g = r x = y
86 85 eleq1d x = y z = a w = a g = r x B y B
87 86 anbi1d x = y z = a w = a g = r x B y B y B y B
88 87 34 bitrdi x = y z = a w = a g = r x B y B y B
89 simpllr x = y z = a w = a g = r z = a
90 89 eleq1d x = y z = a w = a g = r z B a B
91 simplr x = y z = a w = a g = r w = a
92 91 eleq1d x = y z = a w = a g = r w B a B
93 90 92 anbi12d x = y z = a w = a g = r z B w B a B a B
94 anidm a B a B a B
95 93 94 bitrdi x = y z = a w = a g = r z B w B a B
96 85 oveq1d x = y z = a w = a g = r x H y = y H y
97 96 eleq2d x = y z = a w = a g = r f x H y f y H y
98 simpr x = y z = a w = a g = r g = r
99 89 oveq2d x = y z = a w = a g = r y H z = y H a
100 98 99 eleq12d x = y z = a w = a g = r g y H z r y H a
101 89 91 oveq12d x = y z = a w = a g = r z H w = a H a
102 101 eleq2d x = y z = a w = a g = r k z H w k a H a
103 97 100 102 3anbi123d x = y z = a w = a g = r f x H y g y H z k z H w f y H y r y H a k a H a
104 88 95 103 3anbi123d x = y z = a w = a g = r x B y B z B w B f x H y g y H z k z H w y B a B f y H y r y H a k a H a
105 5 104 syl5bb x = y z = a w = a g = r ψ y B a B f y H y r y H a k a H a
106 105 anbi2d x = y z = a w = a g = r φ ψ φ y B a B f y H y r y H a k a H a
107 89 oveq2d x = y z = a w = a g = r y y · ˙ z = y y · ˙ a
108 eqidd x = y z = a w = a g = r 1 ˙ = 1 ˙
109 107 98 108 oveq123d x = y z = a w = a g = r g y y · ˙ z 1 ˙ = r y y · ˙ a 1 ˙
110 109 98 eqeq12d x = y z = a w = a g = r g y y · ˙ z 1 ˙ = g r y y · ˙ a 1 ˙ = r
111 106 110 imbi12d x = y z = a w = a g = r φ ψ g y y · ˙ z 1 ˙ = g φ y B a B f y H y r y H a k a H a r y y · ˙ a 1 ˙ = r
112 111 sbiedvw x = y z = a w = a r g φ ψ g y y · ˙ z 1 ˙ = g φ y B a B f y H y r y H a k a H a r y y · ˙ a 1 ˙ = r
113 112 sbiedvw x = y z = a a w r g φ ψ g y y · ˙ z 1 ˙ = g φ y B a B f y H y r y H a k a H a r y y · ˙ a 1 ˙ = r
114 113 sbiedvw x = y a z a w r g φ ψ g y y · ˙ z 1 ˙ = g φ y B a B f y H y r y H a k a H a r y y · ˙ a 1 ˙ = r
115 8 sbt r g φ ψ g y y · ˙ z 1 ˙ = g
116 115 sbt a w r g φ ψ g y y · ˙ z 1 ˙ = g
117 116 sbt a z a w r g φ ψ g y y · ˙ z 1 ˙ = g
118 114 117 chvarvv φ y B a B f y H y r y H a k a H a r y y · ˙ a 1 ˙ = r
119 78 79 80 84 118 syl13anc φ y B a B r y H a f y H y k a H a r y y · ˙ a 1 ˙ = r
120 119 ex φ y B a B r y H a f y H y k a H a r y y · ˙ a 1 ˙ = r
121 120 exlimdvv φ y B a B r y H a f k f y H y k a H a r y y · ˙ a 1 ˙ = r
122 77 121 syl5bir φ y B a B r y H a f f y H y k k a H a r y y · ˙ a 1 ˙ = r
123 67 76 122 mp2and φ y B a B r y H a r y y · ˙ a 1 ˙ = r
124 id y = z y = z
125 124 124 oveq12d y = z y H y = z H z
126 125 neeq1d y = z y H y z H z
127 71 3ad2ant1 φ y B a B z B r y H a g a H z y B y H y
128 simp23 φ y B a B z B r y H a g a H z z B
129 126 127 128 rspcdva φ y B a B z B r y H a g a H z z H z
130 n0 z H z k k z H z
131 129 130 sylib φ y B a B z B r y H a g a H z k k z H z
132 eleq1w x = y x B y B
133 132 3anbi1d x = y x B a B z B y B a B z B
134 oveq1 x = y x H a = y H a
135 134 eleq2d x = y r x H a r y H a
136 135 anbi1d x = y r x H a g a H z r y H a g a H z
137 136 anbi1d x = y r x H a g a H z k z H z r y H a g a H z k z H z
138 133 137 anbi12d x = y x B a B z B r x H a g a H z k z H z y B a B z B r y H a g a H z k z H z
139 138 anbi2d x = y φ x B a B z B r x H a g a H z k z H z φ y B a B z B r y H a g a H z k z H z
140 opeq1 x = y x a = y a
141 140 oveq1d x = y x a · ˙ z = y a · ˙ z
142 141 oveqd x = y g x a · ˙ z r = g y a · ˙ z r
143 oveq1 x = y x H z = y H z
144 142 143 eleq12d x = y g x a · ˙ z r x H z g y a · ˙ z r y H z
145 139 144 imbi12d x = y φ x B a B z B r x H a g a H z k z H z g x a · ˙ z r x H z φ y B a B z B r y H a g a H z k z H z g y a · ˙ z r y H z
146 df-3an x B y B z B w B f x H y g y H z k z H w x B y B z B w B f x H y g y H z k z H w
147 5 146 bitri ψ x B y B z B w B f x H y g y H z k z H w
148 simpll y = a w = z f = r y = a
149 148 eleq1d y = a w = z f = r y B a B
150 149 anbi2d y = a w = z f = r x B y B x B a B
151 simplr y = a w = z f = r w = z
152 151 eleq1d y = a w = z f = r w B z B
153 152 anbi2d y = a w = z f = r z B w B z B z B
154 anidm z B z B z B
155 153 154 bitrdi y = a w = z f = r z B w B z B
156 150 155 anbi12d y = a w = z f = r x B y B z B w B x B a B z B
157 df-3an x B a B z B x B a B z B
158 156 157 bitr4di y = a w = z f = r x B y B z B w B x B a B z B
159 simpr y = a w = z f = r f = r
160 148 oveq2d y = a w = z f = r x H y = x H a
161 159 160 eleq12d y = a w = z f = r f x H y r x H a
162 148 oveq1d y = a w = z f = r y H z = a H z
163 162 eleq2d y = a w = z f = r g y H z g a H z
164 151 oveq2d y = a w = z f = r z H w = z H z
165 164 eleq2d y = a w = z f = r k z H w k z H z
166 161 163 165 3anbi123d y = a w = z f = r f x H y g y H z k z H w r x H a g a H z k z H z
167 df-3an r x H a g a H z k z H z r x H a g a H z k z H z
168 166 167 bitrdi y = a w = z f = r f x H y g y H z k z H w r x H a g a H z k z H z
169 158 168 anbi12d y = a w = z f = r x B y B z B w B f x H y g y H z k z H w x B a B z B r x H a g a H z k z H z
170 147 169 syl5bb y = a w = z f = r ψ x B a B z B r x H a g a H z k z H z
171 170 anbi2d y = a w = z f = r φ ψ φ x B a B z B r x H a g a H z k z H z
172 148 opeq2d y = a w = z f = r x y = x a
173 172 oveq1d y = a w = z f = r x y · ˙ z = x a · ˙ z
174 eqidd y = a w = z f = r g = g
175 173 174 159 oveq123d y = a w = z f = r g x y · ˙ z f = g x a · ˙ z r
176 175 eleq1d y = a w = z f = r g x y · ˙ z f x H z g x a · ˙ z r x H z
177 171 176 imbi12d y = a w = z f = r φ ψ g x y · ˙ z f x H z φ x B a B z B r x H a g a H z k z H z g x a · ˙ z r x H z
178 177 sbiedvw y = a w = z r f φ ψ g x y · ˙ z f x H z φ x B a B z B r x H a g a H z k z H z g x a · ˙ z r x H z
179 178 sbiedvw y = a z w r f φ ψ g x y · ˙ z f x H z φ x B a B z B r x H a g a H z k z H z g x a · ˙ z r x H z
180 9 sbt r f φ ψ g x y · ˙ z f x H z
181 180 sbt z w r f φ ψ g x y · ˙ z f x H z
182 179 181 chvarvv φ x B a B z B r x H a g a H z k z H z g x a · ˙ z r x H z
183 145 182 chvarvv φ y B a B z B r y H a g a H z k z H z g y a · ˙ z r y H z
184 183 exp45 φ y B a B z B r y H a g a H z k z H z g y a · ˙ z r y H z
185 184 3imp φ y B a B z B r y H a g a H z k z H z g y a · ˙ z r y H z
186 185 exlimdv φ y B a B z B r y H a g a H z k k z H z g y a · ˙ z r y H z
187 131 186 mpd φ y B a B z B r y H a g a H z g y a · ˙ z r y H z
188 132 anbi1d x = y x B a B y B a B
189 188 anbi1d x = y x B a B z B w B y B a B z B w B
190 135 3anbi1d x = y r x H a g a H z k z H w r y H a g a H z k z H w
191 189 190 3anbi23d x = y φ x B a B z B w B r x H a g a H z k z H w φ y B a B z B w B r y H a g a H z k z H w
192 140 oveq1d x = y x a · ˙ w = y a · ˙ w
193 192 oveqd x = y k a z · ˙ w g x a · ˙ w r = k a z · ˙ w g y a · ˙ w r
194 opeq1 x = y x z = y z
195 194 oveq1d x = y x z · ˙ w = y z · ˙ w
196 eqidd x = y k = k
197 195 196 142 oveq123d x = y k x z · ˙ w g x a · ˙ z r = k y z · ˙ w g y a · ˙ z r
198 193 197 eqeq12d x = y k a z · ˙ w g x a · ˙ w r = k x z · ˙ w g x a · ˙ z r k a z · ˙ w g y a · ˙ w r = k y z · ˙ w g y a · ˙ z r
199 191 198 imbi12d x = y φ x B a B z B w B r x H a g a H z k z H w k a z · ˙ w g x a · ˙ w r = k x z · ˙ w g x a · ˙ z r φ y B a B z B w B r y H a g a H z k z H w k a z · ˙ w g y a · ˙ w r = k y z · ˙ w g y a · ˙ z r
200 simpl y = a f = r y = a
201 200 eleq1d y = a f = r y B a B
202 201 anbi2d y = a f = r x B y B x B a B
203 simpr y = a f = r f = r
204 200 oveq2d y = a f = r x H y = x H a
205 203 204 eleq12d y = a f = r f x H y r x H a
206 200 oveq1d y = a f = r y H z = a H z
207 206 eleq2d y = a f = r g y H z g a H z
208 205 207 3anbi12d y = a f = r f x H y g y H z k z H w r x H a g a H z k z H w
209 202 208 3anbi13d y = a f = r x B y B z B w B f x H y g y H z k z H w x B a B z B w B r x H a g a H z k z H w
210 5 209 syl5bb y = a f = r ψ x B a B z B w B r x H a g a H z k z H w
211 df-3an x B a B z B w B r x H a g a H z k z H w x B a B z B w B r x H a g a H z k z H w
212 210 211 bitrdi y = a f = r ψ x B a B z B w B r x H a g a H z k z H w
213 212 anbi2d y = a f = r φ ψ φ x B a B z B w B r x H a g a H z k z H w
214 3anass φ x B a B z B w B r x H a g a H z k z H w φ x B a B z B w B r x H a g a H z k z H w
215 213 214 bitr4di y = a f = r φ ψ φ x B a B z B w B r x H a g a H z k z H w
216 200 opeq2d y = a f = r x y = x a
217 216 oveq1d y = a f = r x y · ˙ w = x a · ˙ w
218 200 opeq1d y = a f = r y z = a z
219 218 oveq1d y = a f = r y z · ˙ w = a z · ˙ w
220 219 oveqd y = a f = r k y z · ˙ w g = k a z · ˙ w g
221 217 220 203 oveq123d y = a f = r k y z · ˙ w g x y · ˙ w f = k a z · ˙ w g x a · ˙ w r
222 216 oveq1d y = a f = r x y · ˙ z = x a · ˙ z
223 eqidd y = a f = r g = g
224 222 223 203 oveq123d y = a f = r g x y · ˙ z f = g x a · ˙ z r
225 224 oveq2d y = a f = r k x z · ˙ w g x y · ˙ z f = k x z · ˙ w g x a · ˙ z r
226 221 225 eqeq12d y = a f = r k y z · ˙ w g x y · ˙ w f = k x z · ˙ w g x y · ˙ z f k a z · ˙ w g x a · ˙ w r = k x z · ˙ w g x a · ˙ z r
227 215 226 imbi12d y = a f = r φ ψ k y z · ˙ w g x y · ˙ w f = k x z · ˙ w g x y · ˙ z f φ x B a B z B w B r x H a g a H z k z H w k a z · ˙ w g x a · ˙ w r = k x z · ˙ w g x a · ˙ z r
228 227 sbiedvw y = a r f φ ψ k y z · ˙ w g x y · ˙ w f = k x z · ˙ w g x y · ˙ z f φ x B a B z B w B r x H a g a H z k z H w k a z · ˙ w g x a · ˙ w r = k x z · ˙ w g x a · ˙ z r
229 10 sbt r f φ ψ k y z · ˙ w g x y · ˙ w f = k x z · ˙ w g x y · ˙ z f
230 228 229 chvarvv φ x B a B z B w B r x H a g a H z k z H w k a z · ˙ w g x a · ˙ w r = k x z · ˙ w g x a · ˙ z r
231 199 230 chvarvv φ y B a B z B w B r y H a g a H z k z H w k a z · ˙ w g y a · ˙ w r = k y z · ˙ w g y a · ˙ z r
232 1 2 3 4 6 64 123 187 231 iscatd φ C Cat
233 1 2 3 232 6 64 123 catidd φ Id C = y B 1 ˙
234 232 233 jca φ C Cat Id C = y B 1 ˙