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 
|- .x. = ( comp ` C )
comfeq.2 
|- .xb = ( comp ` D )
comfeq.h 
|- H = ( Hom ` C )
comfeq.3 
|- ( ph -> B = ( Base ` C ) )
comfeq.4 
|- ( ph -> B = ( Base ` D ) )
comfeq.5 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
Assertion comfeq 
|- ( ph -> ( ( comf ` C ) = ( comf ` D ) <-> A. x e. B A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. .x. z ) f ) = ( g ( <. x , y >. .xb z ) f ) ) )

Proof

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