Metamath Proof Explorer


Theorem comfeq

Description: Condition for two categories with the same hom-sets to have the same composition. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses comfeq.1 · ˙ = comp C
comfeq.2 ˙ = comp D
comfeq.h H = Hom C
comfeq.3 φ B = Base C
comfeq.4 φ B = Base D
comfeq.5 φ Hom 𝑓 C = Hom 𝑓 D
Assertion comfeq φ comp 𝑓 C = comp 𝑓 D x B y B z B f x H y g y H z g x y · ˙ z f = g x y ˙ z f

Proof

Step Hyp Ref Expression
1 comfeq.1 · ˙ = comp C
2 comfeq.2 ˙ = comp D
3 comfeq.h H = Hom C
4 comfeq.3 φ B = Base C
5 comfeq.4 φ B = Base D
6 comfeq.5 φ Hom 𝑓 C = Hom 𝑓 D
7 4 sqxpeqd φ B × B = Base C × Base C
8 eqidd φ g 2 nd u H z , f H u g u · ˙ z f = g 2 nd u H z , f H u g u · ˙ z f
9 7 4 8 mpoeq123dv φ u B × B , z B g 2 nd u H z , f H u g u · ˙ z f = u Base C × Base C , z Base C g 2 nd u H z , f H u g u · ˙ z f
10 eqid comp 𝑓 C = comp 𝑓 C
11 eqid Base C = Base C
12 10 11 3 1 comfffval comp 𝑓 C = u Base C × Base C , z Base C g 2 nd u H z , f H u g u · ˙ z f
13 9 12 syl6eqr φ u B × B , z B g 2 nd u H z , f H u g u · ˙ z f = comp 𝑓 C
14 eqid Hom D = Hom D
15 6 3ad2ant1 φ u B × B z B Hom 𝑓 C = Hom 𝑓 D
16 xp2nd u B × B 2 nd u B
17 16 3ad2ant2 φ u B × B z B 2 nd u B
18 4 3ad2ant1 φ u B × B z B B = Base C
19 17 18 eleqtrd φ u B × B z B 2 nd u Base C
20 simp3 φ u B × B z B z B
21 20 18 eleqtrd φ u B × B z B z Base C
22 11 3 14 15 19 21 homfeqval φ u B × B z B 2 nd u H z = 2 nd u Hom D z
23 xp1st u B × B 1 st u B
24 23 3ad2ant2 φ u B × B z B 1 st u B
25 24 18 eleqtrd φ u B × B z B 1 st u Base C
26 11 3 14 15 25 19 homfeqval φ u B × B z B 1 st u H 2 nd u = 1 st u Hom D 2 nd u
27 df-ov 1 st u H 2 nd u = H 1 st u 2 nd u
28 df-ov 1 st u Hom D 2 nd u = Hom D 1 st u 2 nd u
29 26 27 28 3eqtr3g φ u B × B z B H 1 st u 2 nd u = Hom D 1 st u 2 nd u
30 1st2nd2 u B × B u = 1 st u 2 nd u
31 30 3ad2ant2 φ u B × B z B u = 1 st u 2 nd u
32 31 fveq2d φ u B × B z B H u = H 1 st u 2 nd u
33 31 fveq2d φ u B × B z B Hom D u = Hom D 1 st u 2 nd u
34 29 32 33 3eqtr4d φ u B × B z B H u = Hom D u
35 eqidd φ u B × B z B g u ˙ z f = g u ˙ z f
36 22 34 35 mpoeq123dv φ u B × B z B g 2 nd u H z , f H u g u ˙ z f = g 2 nd u Hom D z , f Hom D u g u ˙ z f
37 36 mpoeq3dva φ u B × B , z B g 2 nd u H z , f H u g u ˙ z f = u B × B , z B g 2 nd u Hom D z , f Hom D u g u ˙ z f
38 5 sqxpeqd φ B × B = Base D × Base D
39 eqidd φ g 2 nd u Hom D z , f Hom D u g u ˙ z f = g 2 nd u Hom D z , f Hom D u g u ˙ z f
40 38 5 39 mpoeq123dv φ u B × B , z B g 2 nd u Hom D z , f Hom D u g u ˙ z f = u Base D × Base D , z Base D g 2 nd u Hom D z , f Hom D u g u ˙ z f
41 37 40 eqtrd φ u B × B , z B g 2 nd u H z , f H u g u ˙ z f = u Base D × Base D , z Base D g 2 nd u Hom D z , f Hom D u g u ˙ z f
42 eqid comp 𝑓 D = comp 𝑓 D
43 eqid Base D = Base D
44 42 43 14 2 comfffval comp 𝑓 D = u Base D × Base D , z Base D g 2 nd u Hom D z , f Hom D u g u ˙ z f
45 41 44 syl6eqr φ u B × B , z B g 2 nd u H z , f H u g u ˙ z f = comp 𝑓 D
46 13 45 eqeq12d φ u B × B , z B g 2 nd u H z , f H u g u · ˙ z f = u B × B , z B g 2 nd u H z , f H u g u ˙ z f comp 𝑓 C = comp 𝑓 D
47 ovex 2 nd u H z V
48 fvex H u V
49 47 48 mpoex g 2 nd u H z , f H u g u · ˙ z f V
50 49 rgen2w u B × B z B g 2 nd u H z , f H u g u · ˙ z f V
51 mpo2eqb u B × B z B g 2 nd u H z , f H u g u · ˙ z f V u B × B , z B g 2 nd u H z , f H u g u · ˙ z f = u B × B , z B g 2 nd u H z , f H u g u ˙ z f u B × B z B g 2 nd u H z , f H u g u · ˙ z f = g 2 nd u H z , f H u g u ˙ z f
52 50 51 ax-mp u B × B , z B g 2 nd u H z , f H u g u · ˙ z f = u B × B , z B g 2 nd u H z , f H u g u ˙ z f u B × B z B g 2 nd u H z , f H u g u · ˙ z f = g 2 nd u H z , f H u g u ˙ z f
53 vex x V
54 vex y V
55 53 54 op2ndd u = x y 2 nd u = y
56 55 oveq1d u = x y 2 nd u H z = y H z
57 fveq2 u = x y H u = H x y
58 df-ov x H y = H x y
59 57 58 syl6eqr u = x y H u = x H y
60 oveq1 u = x y u · ˙ z = x y · ˙ z
61 60 oveqd u = x y g u · ˙ z f = g x y · ˙ z f
62 oveq1 u = x y u ˙ z = x y ˙ z
63 62 oveqd u = x y g u ˙ z f = g x y ˙ z f
64 61 63 eqeq12d u = x y g u · ˙ z f = g u ˙ z f g x y · ˙ z f = g x y ˙ z f
65 59 64 raleqbidv u = x y f H u g u · ˙ z f = g u ˙ z f f x H y g x y · ˙ z f = g x y ˙ z f
66 56 65 raleqbidv u = x y g 2 nd u H z f H u g u · ˙ z f = g u ˙ z f g y H z f x H y g x y · ˙ z f = g x y ˙ z f
67 ovex g u · ˙ z f V
68 67 rgen2w g 2 nd u H z f H u g u · ˙ z f V
69 mpo2eqb g 2 nd u H z f H u g u · ˙ z f V g 2 nd u H z , f H u g u · ˙ z f = g 2 nd u H z , f H u g u ˙ z f g 2 nd u H z f H u g u · ˙ z f = g u ˙ z f
70 68 69 ax-mp g 2 nd u H z , f H u g u · ˙ z f = g 2 nd u H z , f H u g u ˙ z f g 2 nd u H z f H u g u · ˙ z f = g u ˙ z f
71 ralcom f x H y g y H z g x y · ˙ z f = g x y ˙ z f g y H z f x H y g x y · ˙ z f = g x y ˙ z f
72 66 70 71 3bitr4g u = x y g 2 nd u H z , f H u g u · ˙ z f = g 2 nd u H z , f H u g u ˙ z f f x H y g y H z g x y · ˙ z f = g x y ˙ z f
73 72 ralbidv u = x y z B g 2 nd u H z , f H u g u · ˙ z f = g 2 nd u H z , f H u g u ˙ z f z B f x H y g y H z g x y · ˙ z f = g x y ˙ z f
74 73 ralxp u B × B z B g 2 nd u H z , f H u g u · ˙ z f = g 2 nd u H z , f H u g u ˙ z f x B y B z B f x H y g y H z g x y · ˙ z f = g x y ˙ z f
75 52 74 bitri u B × B , z B g 2 nd u H z , f H u g u · ˙ z f = u B × B , z B g 2 nd u H z , f H u g u ˙ z f x B y B z B f x H y g y H z g x y · ˙ z f = g x y ˙ z f
76 46 75 bitr3di φ comp 𝑓 C = comp 𝑓 D x B y B z B f x H y g y H z g x y · ˙ z f = g x y ˙ z f