Metamath Proof Explorer


Theorem xpcval

Description: Value of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017)

Ref Expression
Hypotheses xpcval.t T = C × c D
xpcval.x X = Base C
xpcval.y Y = Base D
xpcval.h H = Hom C
xpcval.j J = Hom D
xpcval.o1 · ˙ = comp C
xpcval.o2 ˙ = comp D
xpcval.c φ C V
xpcval.d φ D W
xpcval.b φ B = X × Y
xpcval.k φ K = u B , v B 1 st u H 1 st v × 2 nd u J 2 nd v
xpcval.o φ O = x B × B , y B g 2 nd x K y , f K x 1 st g 1 st 1 st x 1 st 2 nd x · ˙ 1 st y 1 st f 2 nd g 2 nd 1 st x 2 nd 2 nd x ˙ 2 nd y 2 nd f
Assertion xpcval φ T = Base ndx B Hom ndx K comp ndx O

Proof

Step Hyp Ref Expression
1 xpcval.t T = C × c D
2 xpcval.x X = Base C
3 xpcval.y Y = Base D
4 xpcval.h H = Hom C
5 xpcval.j J = Hom D
6 xpcval.o1 · ˙ = comp C
7 xpcval.o2 ˙ = comp D
8 xpcval.c φ C V
9 xpcval.d φ D W
10 xpcval.b φ B = X × Y
11 xpcval.k φ K = u B , v B 1 st u H 1 st v × 2 nd u J 2 nd v
12 xpcval.o φ O = x B × B , y B g 2 nd x K y , f K x 1 st g 1 st 1 st x 1 st 2 nd x · ˙ 1 st y 1 st f 2 nd g 2 nd 1 st x 2 nd 2 nd x ˙ 2 nd y 2 nd f
13 df-xpc × c = r V , s V Base r × Base s / b u b , v b 1 st u Hom r 1 st v × 2 nd u Hom s 2 nd v / h Base ndx b Hom ndx h comp ndx x b × b , y b g 2 nd x h y , f h x 1 st g 1 st 1 st x 1 st 2 nd x comp r 1 st y 1 st f 2 nd g 2 nd 1 st x 2 nd 2 nd x comp s 2 nd y 2 nd f
14 13 a1i φ × c = r V , s V Base r × Base s / b u b , v b 1 st u Hom r 1 st v × 2 nd u Hom s 2 nd v / h Base ndx b Hom ndx h comp ndx x b × b , y b g 2 nd x h y , f h x 1 st g 1 st 1 st x 1 st 2 nd x comp r 1 st y 1 st f 2 nd g 2 nd 1 st x 2 nd 2 nd x comp s 2 nd y 2 nd f
15 fvex Base r V
16 fvex Base s V
17 15 16 xpex Base r × Base s V
18 17 a1i φ r = C s = D Base r × Base s V
19 simprl φ r = C s = D r = C
20 19 fveq2d φ r = C s = D Base r = Base C
21 20 2 syl6eqr φ r = C s = D Base r = X
22 simprr φ r = C s = D s = D
23 22 fveq2d φ r = C s = D Base s = Base D
24 23 3 syl6eqr φ r = C s = D Base s = Y
25 21 24 xpeq12d φ r = C s = D Base r × Base s = X × Y
26 10 adantr φ r = C s = D B = X × Y
27 25 26 eqtr4d φ r = C s = D Base r × Base s = B
28 vex b V
29 28 28 mpoex u b , v b 1 st u Hom r 1 st v × 2 nd u Hom s 2 nd v V
30 29 a1i φ r = C s = D b = B u b , v b 1 st u Hom r 1 st v × 2 nd u Hom s 2 nd v V
31 simpr φ r = C s = D b = B b = B
32 simplrl φ r = C s = D b = B r = C
33 32 fveq2d φ r = C s = D b = B Hom r = Hom C
34 33 4 syl6eqr φ r = C s = D b = B Hom r = H
35 34 oveqd φ r = C s = D b = B 1 st u Hom r 1 st v = 1 st u H 1 st v
36 simplrr φ r = C s = D b = B s = D
37 36 fveq2d φ r = C s = D b = B Hom s = Hom D
38 37 5 syl6eqr φ r = C s = D b = B Hom s = J
39 38 oveqd φ r = C s = D b = B 2 nd u Hom s 2 nd v = 2 nd u J 2 nd v
40 35 39 xpeq12d φ r = C s = D b = B 1 st u Hom r 1 st v × 2 nd u Hom s 2 nd v = 1 st u H 1 st v × 2 nd u J 2 nd v
41 31 31 40 mpoeq123dv φ r = C s = D b = B u b , v b 1 st u Hom r 1 st v × 2 nd u Hom s 2 nd v = u B , v B 1 st u H 1 st v × 2 nd u J 2 nd v
42 11 ad2antrr φ r = C s = D b = B K = u B , v B 1 st u H 1 st v × 2 nd u J 2 nd v
43 41 42 eqtr4d φ r = C s = D b = B u b , v b 1 st u Hom r 1 st v × 2 nd u Hom s 2 nd v = K
44 simplr φ r = C s = D b = B h = K b = B
45 44 opeq2d φ r = C s = D b = B h = K Base ndx b = Base ndx B
46 simpr φ r = C s = D b = B h = K h = K
47 46 opeq2d φ r = C s = D b = B h = K Hom ndx h = Hom ndx K
48 44 44 xpeq12d φ r = C s = D b = B h = K b × b = B × B
49 46 oveqd φ r = C s = D b = B h = K 2 nd x h y = 2 nd x K y
50 46 fveq1d φ r = C s = D b = B h = K h x = K x
51 32 adantr φ r = C s = D b = B h = K r = C
52 51 fveq2d φ r = C s = D b = B h = K comp r = comp C
53 52 6 syl6eqr φ r = C s = D b = B h = K comp r = · ˙
54 53 oveqd φ r = C s = D b = B h = K 1 st 1 st x 1 st 2 nd x comp r 1 st y = 1 st 1 st x 1 st 2 nd x · ˙ 1 st y
55 54 oveqd φ r = C s = D b = B h = K 1 st g 1 st 1 st x 1 st 2 nd x comp r 1 st y 1 st f = 1 st g 1 st 1 st x 1 st 2 nd x · ˙ 1 st y 1 st f
56 36 adantr φ r = C s = D b = B h = K s = D
57 56 fveq2d φ r = C s = D b = B h = K comp s = comp D
58 57 7 syl6eqr φ r = C s = D b = B h = K comp s = ˙
59 58 oveqd φ r = C s = D b = B h = K 2 nd 1 st x 2 nd 2 nd x comp s 2 nd y = 2 nd 1 st x 2 nd 2 nd x ˙ 2 nd y
60 59 oveqd φ r = C s = D b = B h = K 2 nd g 2 nd 1 st x 2 nd 2 nd x comp s 2 nd y 2 nd f = 2 nd g 2 nd 1 st x 2 nd 2 nd x ˙ 2 nd y 2 nd f
61 55 60 opeq12d φ r = C s = D b = B h = K 1 st g 1 st 1 st x 1 st 2 nd x comp r 1 st y 1 st f 2 nd g 2 nd 1 st x 2 nd 2 nd x comp s 2 nd y 2 nd f = 1 st g 1 st 1 st x 1 st 2 nd x · ˙ 1 st y 1 st f 2 nd g 2 nd 1 st x 2 nd 2 nd x ˙ 2 nd y 2 nd f
62 49 50 61 mpoeq123dv φ r = C s = D b = B h = K g 2 nd x h y , f h x 1 st g 1 st 1 st x 1 st 2 nd x comp r 1 st y 1 st f 2 nd g 2 nd 1 st x 2 nd 2 nd x comp s 2 nd y 2 nd f = g 2 nd x K y , f K x 1 st g 1 st 1 st x 1 st 2 nd x · ˙ 1 st y 1 st f 2 nd g 2 nd 1 st x 2 nd 2 nd x ˙ 2 nd y 2 nd f
63 48 44 62 mpoeq123dv φ r = C s = D b = B h = K x b × b , y b g 2 nd x h y , f h x 1 st g 1 st 1 st x 1 st 2 nd x comp r 1 st y 1 st f 2 nd g 2 nd 1 st x 2 nd 2 nd x comp s 2 nd y 2 nd f = x B × B , y B g 2 nd x K y , f K x 1 st g 1 st 1 st x 1 st 2 nd x · ˙ 1 st y 1 st f 2 nd g 2 nd 1 st x 2 nd 2 nd x ˙ 2 nd y 2 nd f
64 12 ad3antrrr φ r = C s = D b = B h = K O = x B × B , y B g 2 nd x K y , f K x 1 st g 1 st 1 st x 1 st 2 nd x · ˙ 1 st y 1 st f 2 nd g 2 nd 1 st x 2 nd 2 nd x ˙ 2 nd y 2 nd f
65 63 64 eqtr4d φ r = C s = D b = B h = K x b × b , y b g 2 nd x h y , f h x 1 st g 1 st 1 st x 1 st 2 nd x comp r 1 st y 1 st f 2 nd g 2 nd 1 st x 2 nd 2 nd x comp s 2 nd y 2 nd f = O
66 65 opeq2d φ r = C s = D b = B h = K comp ndx x b × b , y b g 2 nd x h y , f h x 1 st g 1 st 1 st x 1 st 2 nd x comp r 1 st y 1 st f 2 nd g 2 nd 1 st x 2 nd 2 nd x comp s 2 nd y 2 nd f = comp ndx O
67 45 47 66 tpeq123d φ r = C s = D b = B h = K Base ndx b Hom ndx h comp ndx x b × b , y b g 2 nd x h y , f h x 1 st g 1 st 1 st x 1 st 2 nd x comp r 1 st y 1 st f 2 nd g 2 nd 1 st x 2 nd 2 nd x comp s 2 nd y 2 nd f = Base ndx B Hom ndx K comp ndx O
68 30 43 67 csbied2 φ r = C s = D b = B u b , v b 1 st u Hom r 1 st v × 2 nd u Hom s 2 nd v / h Base ndx b Hom ndx h comp ndx x b × b , y b g 2 nd x h y , f h x 1 st g 1 st 1 st x 1 st 2 nd x comp r 1 st y 1 st f 2 nd g 2 nd 1 st x 2 nd 2 nd x comp s 2 nd y 2 nd f = Base ndx B Hom ndx K comp ndx O
69 18 27 68 csbied2 φ r = C s = D Base r × Base s / b u b , v b 1 st u Hom r 1 st v × 2 nd u Hom s 2 nd v / h Base ndx b Hom ndx h comp ndx x b × b , y b g 2 nd x h y , f h x 1 st g 1 st 1 st x 1 st 2 nd x comp r 1 st y 1 st f 2 nd g 2 nd 1 st x 2 nd 2 nd x comp s 2 nd y 2 nd f = Base ndx B Hom ndx K comp ndx O
70 8 elexd φ C V
71 9 elexd φ D V
72 tpex Base ndx B Hom ndx K comp ndx O V
73 72 a1i φ Base ndx B Hom ndx K comp ndx O V
74 14 69 70 71 73 ovmpod φ C × c D = Base ndx B Hom ndx K comp ndx O
75 1 74 syl5eq φ T = Base ndx B Hom ndx K comp ndx O