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 ) ) )