Metamath Proof Explorer


Theorem xpcco

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

Ref Expression
Hypotheses xpccofval.t T = C × c D
xpccofval.b B = Base T
xpccofval.k K = Hom T
xpccofval.o1 · ˙ = comp C
xpccofval.o2 ˙ = comp D
xpccofval.o O = comp T
xpcco.x φ X B
xpcco.y φ Y B
xpcco.z φ Z B
xpcco.f φ F X K Y
xpcco.g φ G Y K Z
Assertion xpcco φ G X Y O Z F = 1 st G 1 st X 1 st Y · ˙ 1 st Z 1 st F 2 nd G 2 nd X 2 nd Y ˙ 2 nd Z 2 nd F

Proof

Step Hyp Ref Expression
1 xpccofval.t T = C × c D
2 xpccofval.b B = Base T
3 xpccofval.k K = Hom T
4 xpccofval.o1 · ˙ = comp C
5 xpccofval.o2 ˙ = comp D
6 xpccofval.o O = comp T
7 xpcco.x φ X B
8 xpcco.y φ Y B
9 xpcco.z φ Z B
10 xpcco.f φ F X K Y
11 xpcco.g φ G Y K Z
12 1 2 3 4 5 6 xpccofval 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 7 8 opelxpd φ X Y B × B
14 9 adantr φ x = X Y Z B
15 ovex 2 nd x K y V
16 fvex K x V
17 15 16 mpoex 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 V
18 17 a1i φ x = X Y y = Z 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 V
19 11 adantr φ x = X Y y = Z G Y K Z
20 simprl φ x = X Y y = Z x = X Y
21 20 fveq2d φ x = X Y y = Z 2 nd x = 2 nd X Y
22 op2ndg X B Y B 2 nd X Y = Y
23 7 8 22 syl2anc φ 2 nd X Y = Y
24 23 adantr φ x = X Y y = Z 2 nd X Y = Y
25 21 24 eqtrd φ x = X Y y = Z 2 nd x = Y
26 simprr φ x = X Y y = Z y = Z
27 25 26 oveq12d φ x = X Y y = Z 2 nd x K y = Y K Z
28 19 27 eleqtrrd φ x = X Y y = Z G 2 nd x K y
29 10 adantr φ x = X Y y = Z F X K Y
30 20 fveq2d φ x = X Y y = Z K x = K X Y
31 df-ov X K Y = K X Y
32 30 31 eqtr4di φ x = X Y y = Z K x = X K Y
33 29 32 eleqtrrd φ x = X Y y = Z F K x
34 33 adantr φ x = X Y y = Z g = G F K x
35 opex 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 V
36 35 a1i φ x = X Y y = Z g = G f = 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 V
37 20 fveq2d φ x = X Y y = Z 1 st x = 1 st X Y
38 op1stg X B Y B 1 st X Y = X
39 7 8 38 syl2anc φ 1 st X Y = X
40 39 adantr φ x = X Y y = Z 1 st X Y = X
41 37 40 eqtrd φ x = X Y y = Z 1 st x = X
42 41 adantr φ x = X Y y = Z g = G f = F 1 st x = X
43 42 fveq2d φ x = X Y y = Z g = G f = F 1 st 1 st x = 1 st X
44 25 adantr φ x = X Y y = Z g = G f = F 2 nd x = Y
45 44 fveq2d φ x = X Y y = Z g = G f = F 1 st 2 nd x = 1 st Y
46 43 45 opeq12d φ x = X Y y = Z g = G f = F 1 st 1 st x 1 st 2 nd x = 1 st X 1 st Y
47 simplrr φ x = X Y y = Z g = G f = F y = Z
48 47 fveq2d φ x = X Y y = Z g = G f = F 1 st y = 1 st Z
49 46 48 oveq12d φ x = X Y y = Z g = G f = F 1 st 1 st x 1 st 2 nd x · ˙ 1 st y = 1 st X 1 st Y · ˙ 1 st Z
50 simprl φ x = X Y y = Z g = G f = F g = G
51 50 fveq2d φ x = X Y y = Z g = G f = F 1 st g = 1 st G
52 simprr φ x = X Y y = Z g = G f = F f = F
53 52 fveq2d φ x = X Y y = Z g = G f = F 1 st f = 1 st F
54 49 51 53 oveq123d φ x = X Y y = Z g = G f = F 1 st g 1 st 1 st x 1 st 2 nd x · ˙ 1 st y 1 st f = 1 st G 1 st X 1 st Y · ˙ 1 st Z 1 st F
55 42 fveq2d φ x = X Y y = Z g = G f = F 2 nd 1 st x = 2 nd X
56 44 fveq2d φ x = X Y y = Z g = G f = F 2 nd 2 nd x = 2 nd Y
57 55 56 opeq12d φ x = X Y y = Z g = G f = F 2 nd 1 st x 2 nd 2 nd x = 2 nd X 2 nd Y
58 47 fveq2d φ x = X Y y = Z g = G f = F 2 nd y = 2 nd Z
59 57 58 oveq12d φ x = X Y y = Z g = G f = F 2 nd 1 st x 2 nd 2 nd x ˙ 2 nd y = 2 nd X 2 nd Y ˙ 2 nd Z
60 50 fveq2d φ x = X Y y = Z g = G f = F 2 nd g = 2 nd G
61 52 fveq2d φ x = X Y y = Z g = G f = F 2 nd f = 2 nd F
62 59 60 61 oveq123d φ x = X Y y = Z g = G f = F 2 nd g 2 nd 1 st x 2 nd 2 nd x ˙ 2 nd y 2 nd f = 2 nd G 2 nd X 2 nd Y ˙ 2 nd Z 2 nd F
63 54 62 opeq12d φ x = X Y y = Z g = G f = 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 = 1 st G 1 st X 1 st Y · ˙ 1 st Z 1 st F 2 nd G 2 nd X 2 nd Y ˙ 2 nd Z 2 nd F
64 28 34 36 63 ovmpodv2 φ x = X Y y = Z X Y O Z = 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 G X Y O Z F = 1 st G 1 st X 1 st Y · ˙ 1 st Z 1 st F 2 nd G 2 nd X 2 nd Y ˙ 2 nd Z 2 nd F
65 13 14 18 64 ovmpodv φ 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 G X Y O Z F = 1 st G 1 st X 1 st Y · ˙ 1 st Z 1 st F 2 nd G 2 nd X 2 nd Y ˙ 2 nd Z 2 nd F
66 12 65 mpi φ G X Y O Z F = 1 st G 1 st X 1 st Y · ˙ 1 st Z 1 st F 2 nd G 2 nd X 2 nd Y ˙ 2 nd Z 2 nd F