MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  funcpropd Unicode version

Theorem funcpropd 13790
Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same functors. (Contributed by Mario Carneiro, 17-Jan-2017.)
Hypotheses
Ref Expression
funcpropd.1  |-  ( ph  ->  (  Homf 
`  A )  =  (  Homf 
`  B ) )
funcpropd.2  |-  ( ph  ->  (compf `  A )  =  (compf `  B ) )
funcpropd.3  |-  ( ph  ->  (  Homf 
`  C )  =  (  Homf 
`  D ) )
funcpropd.4  |-  ( ph  ->  (compf `  C )  =  (compf `  D ) )
funcpropd.a  |-  ( ph  ->  A  e.  V )
funcpropd.b  |-  ( ph  ->  B  e.  V )
funcpropd.c  |-  ( ph  ->  C  e.  V )
funcpropd.d  |-  ( ph  ->  D  e.  V )
Assertion
Ref Expression
funcpropd  |-  ( ph  ->  ( A  Func  C
)  =  ( B 
Func  D ) )

Proof of Theorem funcpropd
Dummy variables  f 
g  m  n  w  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relfunc 13752 . . 3  |-  Rel  ( A  Func  C )
21a1i 10 . 2  |-  ( ph  ->  Rel  ( A  Func  C ) )
3 relfunc 13752 . . 3  |-  Rel  ( B  Func  D )
43a1i 10 . 2  |-  ( ph  ->  Rel  ( B  Func  D ) )
5 funcpropd.1 . . . . . 6  |-  ( ph  ->  (  Homf 
`  A )  =  (  Homf 
`  B ) )
6 funcpropd.2 . . . . . 6  |-  ( ph  ->  (compf `  A )  =  (compf `  B ) )
7 funcpropd.a . . . . . 6  |-  ( ph  ->  A  e.  V )
8 funcpropd.b . . . . . 6  |-  ( ph  ->  B  e.  V )
95, 6, 7, 8catpropd 13628 . . . . 5  |-  ( ph  ->  ( A  e.  Cat  <->  B  e.  Cat ) )
10 funcpropd.3 . . . . . 6  |-  ( ph  ->  (  Homf 
`  C )  =  (  Homf 
`  D ) )
11 funcpropd.4 . . . . . 6  |-  ( ph  ->  (compf `  C )  =  (compf `  D ) )
12 funcpropd.c . . . . . 6  |-  ( ph  ->  C  e.  V )
13 funcpropd.d . . . . . 6  |-  ( ph  ->  D  e.  V )
1410, 11, 12, 13catpropd 13628 . . . . 5  |-  ( ph  ->  ( C  e.  Cat  <->  D  e.  Cat ) )
159, 14anbi12d 691 . . . 4  |-  ( ph  ->  ( ( A  e. 
Cat  /\  C  e.  Cat )  <->  ( B  e. 
Cat  /\  D  e.  Cat ) ) )
16 fveq2 5541 . . . . . . . . . . . . . 14  |-  ( z  =  w  ->  ( 1st `  z )  =  ( 1st `  w
) )
1716fveq2d 5545 . . . . . . . . . . . . 13  |-  ( z  =  w  ->  (
f `  ( 1st `  z ) )  =  ( f `  ( 1st `  w ) ) )
18 fveq2 5541 . . . . . . . . . . . . . 14  |-  ( z  =  w  ->  ( 2nd `  z )  =  ( 2nd `  w
) )
1918fveq2d 5545 . . . . . . . . . . . . 13  |-  ( z  =  w  ->  (
f `  ( 2nd `  z ) )  =  ( f `  ( 2nd `  w ) ) )
2017, 19oveq12d 5892 . . . . . . . . . . . 12  |-  ( z  =  w  ->  (
( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  =  ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) ) )
21 fveq2 5541 . . . . . . . . . . . 12  |-  ( z  =  w  ->  (
(  Hom  `  A ) `
 z )  =  ( (  Hom  `  A
) `  w )
)
2220, 21oveq12d 5892 . . . . . . . . . . 11  |-  ( z  =  w  ->  (
( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) )  =  ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C )
( f `  ( 2nd `  w ) ) )  ^m  ( (  Hom  `  A ) `  w ) ) )
2322cbvixpv 6850 . . . . . . . . . 10  |-  X_ z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) )  =  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) )
2423eleq2i 2360 . . . . . . . . 9  |-  ( g  e.  X_ z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) )  <-> 
g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) )
2524anbi2i 675 . . . . . . . 8  |-  ( ( f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) ) )  <->  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )
265ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  (  Homf  `  A )  =  (  Homf 
`  B ) )
276ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  (compf `  A
)  =  (compf `  B
) )
287ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  A  e.  V )
298ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  B  e.  V )
3026, 27, 28, 29cidpropd 13629 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  ( Id `  A )  =  ( Id `  B
) )
3130fveq1d 5543 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  (
( Id `  A
) `  x )  =  ( ( Id
`  B ) `  x ) )
3231fveq2d 5545 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  (
( x g x ) `  ( ( Id `  A ) `
 x ) )  =  ( ( x g x ) `  ( ( Id `  B ) `  x
) ) )
3310, 11, 12, 13cidpropd 13629 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Id `  C
)  =  ( Id
`  D ) )
3433ad2antrr 706 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  ( Id `  C )  =  ( Id `  D
) )
3534fveq1d 5543 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  (
( Id `  C
) `  ( f `  x ) )  =  ( ( Id `  D ) `  (
f `  x )
) )
3632, 35eqeq12d 2310 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  (
( ( x g x ) `  (
( Id `  A
) `  x )
)  =  ( ( Id `  C ) `
 ( f `  x ) )  <->  ( (
x g x ) `
 ( ( Id
`  B ) `  x ) )  =  ( ( Id `  D ) `  (
f `  x )
) ) )
37 eqid 2296 . . . . . . . . . . . . . . . . . 18  |-  ( Base `  A )  =  (
Base `  A )
38 eqid 2296 . . . . . . . . . . . . . . . . . 18  |-  (  Hom  `  A )  =  (  Hom  `  A )
39 eqid 2296 . . . . . . . . . . . . . . . . . 18  |-  (comp `  A )  =  (comp `  A )
40 eqid 2296 . . . . . . . . . . . . . . . . . 18  |-  (comp `  B )  =  (comp `  B )
4126ad4antr 712 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  (  Homf  `  A
)  =  (  Homf  `  B ) )
4227ad4antr 712 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  (compf `  A )  =  (compf `  B ) )
43 simp-5r 745 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  x  e.  ( Base `  A )
)
44 simp-4r 743 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  y  e.  ( Base `  A )
)
45 simpllr 735 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  z  e.  ( Base `  A )
)
46 simplr 731 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  m  e.  ( x (  Hom  `  A ) y ) )
47 simpr 447 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  n  e.  ( y (  Hom  `  A ) z ) )
4837, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47comfeqval 13627 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  ( n
( <. x ,  y
>. (comp `  A )
z ) m )  =  ( n (
<. x ,  y >.
(comp `  B )
z ) m ) )
4948fveq2d 5545 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  ( (
x g z ) `
 ( n (
<. x ,  y >.
(comp `  A )
z ) m ) )  =  ( ( x g z ) `
 ( n (
<. x ,  y >.
(comp `  B )
z ) m ) ) )
50 eqid 2296 . . . . . . . . . . . . . . . . 17  |-  ( Base `  C )  =  (
Base `  C )
51 eqid 2296 . . . . . . . . . . . . . . . . 17  |-  (  Hom  `  C )  =  (  Hom  `  C )
52 eqid 2296 . . . . . . . . . . . . . . . . 17  |-  (comp `  C )  =  (comp `  C )
53 eqid 2296 . . . . . . . . . . . . . . . . 17  |-  (comp `  D )  =  (comp `  D )
5410ad6antr 716 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  (  Homf  `  C
)  =  (  Homf  `  D ) )
5511ad6antr 716 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  (compf `  C )  =  (compf `  D ) )
56 simprl 732 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  ->  f : ( Base `  A
) --> ( Base `  C
) )
5756ad5antr 714 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  f :
( Base `  A ) --> ( Base `  C )
)
5857, 43ffvelrnd 5682 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  ( f `  x )  e.  (
Base `  C )
)
5957, 44ffvelrnd 5682 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  ( f `  y )  e.  (
Base `  C )
)
6057, 45ffvelrnd 5682 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  ( f `  z )  e.  (
Base `  C )
)
61 df-ov 5877 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x g y )  =  ( g `  <. x ,  y >. )
62 simprr 733 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  ->  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) )
6362ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) )
6463adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  ->  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) )
65 simp-4r 743 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  ->  x  e.  ( Base `  A )
)
66 simpllr 735 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  ->  y  e.  ( Base `  A )
)
67 opelxpi 4737 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  ( Base `  A )  /\  y  e.  ( Base `  A
) )  ->  <. x ,  y >.  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )
6865, 66, 67syl2anc 642 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  ->  <. x ,  y >.  e.  (
( Base `  A )  X.  ( Base `  A
) ) )
69 vex 2804 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  x  e. 
_V
70 vex 2804 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  y  e. 
_V
7169, 70op1std 6146 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  =  <. x ,  y
>.  ->  ( 1st `  w
)  =  x )
7271fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  <. x ,  y
>.  ->  ( f `  ( 1st `  w ) )  =  ( f `
 x ) )
7369, 70op2ndd 6147 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  =  <. x ,  y
>.  ->  ( 2nd `  w
)  =  y )
7473fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  <. x ,  y
>.  ->  ( f `  ( 2nd `  w ) )  =  ( f `
 y ) )
7572, 74oveq12d 5892 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  =  <. x ,  y
>.  ->  ( ( f `
 ( 1st `  w
) ) (  Hom  `  C ) ( f `
 ( 2nd `  w
) ) )  =  ( ( f `  x ) (  Hom  `  C ) ( f `
 y ) ) )
76 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  <. x ,  y
>.  ->  ( (  Hom  `  A ) `  w
)  =  ( (  Hom  `  A ) `  <. x ,  y
>. ) )
77 df-ov 5877 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x (  Hom  `  A
) y )  =  ( (  Hom  `  A
) `  <. x ,  y >. )
7876, 77syl6eqr 2346 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  =  <. x ,  y
>.  ->  ( (  Hom  `  A ) `  w
)  =  ( x (  Hom  `  A
) y ) )
7975, 78oveq12d 5892 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  =  <. x ,  y
>.  ->  ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C )
( f `  ( 2nd `  w ) ) )  ^m  ( (  Hom  `  A ) `  w ) )  =  ( ( ( f `
 x ) (  Hom  `  C )
( f `  y
) )  ^m  (
x (  Hom  `  A
) y ) ) )
8079fvixp 6837 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) )  /\  <. x ,  y
>.  e.  ( ( Base `  A )  X.  ( Base `  A ) ) )  ->  ( g `  <. x ,  y
>. )  e.  (
( ( f `  x ) (  Hom  `  C ) ( f `
 y ) )  ^m  ( x (  Hom  `  A )
y ) ) )
8164, 68, 80syl2anc 642 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  ->  ( g `  <. x ,  y
>. )  e.  (
( ( f `  x ) (  Hom  `  C ) ( f `
 y ) )  ^m  ( x (  Hom  `  A )
y ) ) )
8261, 81syl5eqel 2380 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  ->  ( x
g y )  e.  ( ( ( f `
 x ) (  Hom  `  C )
( f `  y
) )  ^m  (
x (  Hom  `  A
) y ) ) )
83 elmapi 6808 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x g y )  e.  ( ( ( f `  x ) (  Hom  `  C
) ( f `  y ) )  ^m  ( x (  Hom  `  A ) y ) )  ->  ( x
g y ) : ( x (  Hom  `  A ) y ) --> ( ( f `  x ) (  Hom  `  C ) ( f `
 y ) ) )
8482, 83syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  ->  ( x
g y ) : ( x (  Hom  `  A ) y ) --> ( ( f `  x ) (  Hom  `  C ) ( f `
 y ) ) )
8584adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  ( x
g y ) : ( x (  Hom  `  A ) y ) --> ( ( f `  x ) (  Hom  `  C ) ( f `
 y ) ) )
8685, 46ffvelrnd 5682 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  ( (
x g y ) `
 m )  e.  ( ( f `  x ) (  Hom  `  C ) ( f `
 y ) ) )
87 df-ov 5877 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y g z )  =  ( g `  <. y ,  z >. )
88 opelxpi 4737 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( y  e.  ( Base `  A )  /\  z  e.  ( Base `  A
) )  ->  <. y ,  z >.  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )
8988adantll 694 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  <. y ,  z >.  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )
90 vex 2804 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  z  e. 
_V
9170, 90op1std 6146 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  =  <. y ,  z
>.  ->  ( 1st `  w
)  =  y )
9291fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  <. y ,  z
>.  ->  ( f `  ( 1st `  w ) )  =  ( f `
 y ) )
9370, 90op2ndd 6147 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  =  <. y ,  z
>.  ->  ( 2nd `  w
)  =  z )
9493fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  <. y ,  z
>.  ->  ( f `  ( 2nd `  w ) )  =  ( f `
 z ) )
9592, 94oveq12d 5892 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  =  <. y ,  z
>.  ->  ( ( f `
 ( 1st `  w
) ) (  Hom  `  C ) ( f `
 ( 2nd `  w
) ) )  =  ( ( f `  y ) (  Hom  `  C ) ( f `
 z ) ) )
96 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  <. y ,  z
>.  ->  ( (  Hom  `  A ) `  w
)  =  ( (  Hom  `  A ) `  <. y ,  z
>. ) )
97 df-ov 5877 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y (  Hom  `  A
) z )  =  ( (  Hom  `  A
) `  <. y ,  z >. )
9896, 97syl6eqr 2346 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  =  <. y ,  z
>.  ->  ( (  Hom  `  A ) `  w
)  =  ( y (  Hom  `  A
) z ) )
9995, 98oveq12d 5892 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  =  <. y ,  z
>.  ->  ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C )
( f `  ( 2nd `  w ) ) )  ^m  ( (  Hom  `  A ) `  w ) )  =  ( ( ( f `
 y ) (  Hom  `  C )
( f `  z
) )  ^m  (
y (  Hom  `  A
) z ) ) )
10099fvixp 6837 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) )  /\  <. y ,  z
>.  e.  ( ( Base `  A )  X.  ( Base `  A ) ) )  ->  ( g `  <. y ,  z
>. )  e.  (
( ( f `  y ) (  Hom  `  C ) ( f `
 z ) )  ^m  ( y (  Hom  `  A )
z ) ) )
10163, 89, 100syl2anc 642 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  (
g `  <. y ,  z >. )  e.  ( ( ( f `  y ) (  Hom  `  C ) ( f `
 z ) )  ^m  ( y (  Hom  `  A )
z ) ) )
10287, 101syl5eqel 2380 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  (
y g z )  e.  ( ( ( f `  y ) (  Hom  `  C
) ( f `  z ) )  ^m  ( y (  Hom  `  A ) z ) ) )
103 elmapi 6808 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y g z )  e.  ( ( ( f `  y ) (  Hom  `  C
) ( f `  z ) )  ^m  ( y (  Hom  `  A ) z ) )  ->  ( y
g z ) : ( y (  Hom  `  A ) z ) --> ( ( f `  y ) (  Hom  `  C ) ( f `
 z ) ) )
104102, 103syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  (
y g z ) : ( y (  Hom  `  A )
z ) --> ( ( f `  y ) (  Hom  `  C
) ( f `  z ) ) )
105104adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  ->  ( y
g z ) : ( y (  Hom  `  A ) z ) --> ( ( f `  y ) (  Hom  `  C ) ( f `
 z ) ) )
106105ffvelrnda 5681 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  ( (
y g z ) `
 n )  e.  ( ( f `  y ) (  Hom  `  C ) ( f `
 z ) ) )
10750, 51, 52, 53, 54, 55, 58, 59, 60, 86, 106comfeqval 13627 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  ( (
( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) )  =  ( ( ( y g z ) `
 n ) (
<. ( f `  x
) ,  ( f `
 y ) >.
(comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) )
10849, 107eqeq12d 2310 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  ( (
( x g z ) `  ( n ( <. x ,  y
>. (comp `  A )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) )  <-> 
( ( x g z ) `  (
n ( <. x ,  y >. (comp `  B ) z ) m ) )  =  ( ( ( y g z ) `  n ) ( <.
( f `  x
) ,  ( f `
 y ) >.
(comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )
109108ralbidva 2572 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  ->  ( A. n  e.  ( y
(  Hom  `  A ) z ) ( ( x g z ) `
 ( n (
<. x ,  y >.
(comp `  A )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) )  <->  A. n  e.  (
y (  Hom  `  A
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )
110109ralbidva 2572 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  ( A. m  e.  (
x (  Hom  `  A
) y ) A. n  e.  ( y
(  Hom  `  A ) z ) ( ( x g z ) `
 ( n (
<. x ,  y >.
(comp `  A )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) )  <->  A. m  e.  (
x (  Hom  `  A
) y ) A. n  e.  ( y
(  Hom  `  A ) z ) ( ( x g z ) `
 ( n (
<. x ,  y >.
(comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )
111 eqid 2296 . . . . . . . . . . . . . . 15  |-  (  Hom  `  B )  =  (  Hom  `  B )
11226ad2antrr 706 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  (  Homf  `  A )  =  (  Homf 
`  B ) )
113 simpllr 735 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  x  e.  ( Base `  A
) )
114 simplr 731 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  y  e.  ( Base `  A
) )
11537, 38, 111, 112, 113, 114homfeqval 13616 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  (
x (  Hom  `  A
) y )  =  ( x (  Hom  `  B ) y ) )
116 simpr 447 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  z  e.  ( Base `  A
) )
11737, 38, 111, 112, 114, 116homfeqval 13616 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  (
y (  Hom  `  A
) z )  =  ( y (  Hom  `  B ) z ) )
118117raleqdv 2755 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  ( A. n  e.  (
y (  Hom  `  A
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) )  <->  A. n  e.  (
y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )
119115, 118raleqbidv 2761 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  ( A. m  e.  (
x (  Hom  `  A
) y ) A. n  e.  ( y
(  Hom  `  A ) z ) ( ( x g z ) `
 ( n (
<. x ,  y >.
(comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) )  <->  A. m  e.  (
x (  Hom  `  B
) y ) A. n  e.  ( y
(  Hom  `  B ) z ) ( ( x g z ) `
 ( n (
<. x ,  y >.
(comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )
120110, 119bitrd 244 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  ( A. m  e.  (
x (  Hom  `  A
) y ) A. n  e.  ( y
(  Hom  `  A ) z ) ( ( x g z ) `
 ( n (
<. x ,  y >.
(comp `  A )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) )  <->  A. m  e.  (
x (  Hom  `  B
) y ) A. n  e.  ( y
(  Hom  `  B ) z ) ( ( x g z ) `
 ( n (
<. x ,  y >.
(comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )
121120ralbidva 2572 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  ->  ( A. z  e.  ( Base `  A ) A. m  e.  ( x
(  Hom  `  A ) y ) A. n  e.  ( y (  Hom  `  A ) z ) ( ( x g z ) `  (
n ( <. x ,  y >. (comp `  A ) z ) m ) )  =  ( ( ( y g z ) `  n ) ( <.
( f `  x
) ,  ( f `
 y ) >.
(comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) )  <->  A. z  e.  ( Base `  A ) A. m  e.  ( x
(  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B ) z ) ( ( x g z ) `  (
n ( <. x ,  y >. (comp `  B ) z ) m ) )  =  ( ( ( y g z ) `  n ) ( <.
( f `  x
) ,  ( f `
 y ) >.
(comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )
122121ralbidva 2572 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  ( A. y  e.  ( Base `  A ) A. z  e.  ( Base `  A ) A. m  e.  ( x (  Hom  `  A ) y ) A. n  e.  ( y (  Hom  `  A
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  A )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) )  <->  A. y  e.  ( Base `  A ) A. z  e.  ( Base `  A ) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )
12336, 122anbi12d 691 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  (
( ( ( x g x ) `  ( ( Id `  A ) `  x
) )  =  ( ( Id `  C
) `  ( f `  x ) )  /\  A. y  e.  ( Base `  A ) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  A ) y ) A. n  e.  ( y (  Hom  `  A
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  A )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) ) )  <->  ( ( ( x g x ) `
 ( ( Id
`  B ) `  x ) )  =  ( ( Id `  D ) `  (
f `  x )
)  /\  A. y  e.  ( Base `  A
) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) ) )
124123ralbidva 2572 . . . . . . . 8  |-  ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  ->  ( A. x  e.  ( Base `  A ) ( ( ( x g x ) `  (
( Id `  A
) `  x )
)  =  ( ( Id `  C ) `
 ( f `  x ) )  /\  A. y  e.  ( Base `  A ) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  A ) y ) A. n  e.  ( y (  Hom  `  A
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  A )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) ) )  <->  A. x  e.  (
Base `  A )
( ( ( x g x ) `  ( ( Id `  B ) `  x
) )  =  ( ( Id `  D
) `  ( f `  x ) )  /\  A. y  e.  ( Base `  A ) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) ) )
12525, 124sylan2b 461 . . . . . . 7  |-  ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ z  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) ) ) )  ->  ( A. x  e.  ( Base `  A ) ( ( ( x g x ) `  (
( Id `  A
) `  x )
)  =  ( ( Id `  C ) `
 ( f `  x ) )  /\  A. y  e.  ( Base `  A ) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  A ) y ) A. n  e.  ( y (  Hom  `  A
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  A )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) ) )  <->  A. x  e.  (
Base `  A )
( ( ( x g x ) `  ( ( Id `  B ) `  x
) )  =  ( ( Id `  D
) `  ( f `  x ) )  /\  A. y  e.  ( Base `  A ) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) ) )
126125pm5.32da 622 . . . . . 6  |-  ( ph  ->  ( ( ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ z  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) ) )  /\  A. x  e.  ( Base `  A
) ( ( ( x g x ) `
 ( ( Id
`  A ) `  x ) )  =  ( ( Id `  C ) `  (
f `  x )
)  /\  A. y  e.  ( Base `  A
) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  A ) y ) A. n  e.  ( y (  Hom  `  A
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  A )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )  <->  ( (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) ) )  /\  A. x  e.  ( Base `  A
) ( ( ( x g x ) `
 ( ( Id
`  B ) `  x ) )  =  ( ( Id `  D ) `  (
f `  x )
)  /\  A. y  e.  ( Base `  A
) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) ) ) )
127 eqid 2296 . . . . . . . . . . . . . 14  |-  (  Hom  `  D )  =  (  Hom  `  D )
12810ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  (  Homf  `  C )  =  (  Homf  `  D ) )
129 simplr 731 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  f : (
Base `  A ) --> ( Base `  C )
)
130 xp1st 6165 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( ( Base `  A )  X.  ( Base `  A ) )  ->  ( 1st `  z
)  e.  ( Base `  A ) )
131130adantl 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( 1st `  z
)  e.  ( Base `  A ) )
132129, 131ffvelrnd 5682 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( f `  ( 1st `  z ) )  e.  ( Base `  C ) )
133 xp2nd 6166 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( ( Base `  A )  X.  ( Base `  A ) )  ->  ( 2nd `  z
)  e.  ( Base `  A ) )
134133adantl 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( 2nd `  z
)  e.  ( Base `  A ) )
135129, 134ffvelrnd 5682 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( f `  ( 2nd `  z ) )  e.  ( Base `  C ) )
13650, 51, 127, 128, 132, 135homfeqval 13616 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( ( f `
 ( 1st `  z
) ) (  Hom  `  C ) ( f `
 ( 2nd `  z
) ) )  =  ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) ) )
1375ad2antrr 706 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  (  Homf  `  A )  =  (  Homf  `  B ) )
13837, 38, 111, 137, 131, 134homfeqval 13616 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( ( 1st `  z ) (  Hom  `  A ) ( 2nd `  z ) )  =  ( ( 1st `  z
) (  Hom  `  B
) ( 2nd `  z
) ) )
139 df-ov 5877 . . . . . . . . . . . . . . 15  |-  ( ( 1st `  z ) (  Hom  `  A
) ( 2nd `  z
) )  =  ( (  Hom  `  A
) `  <. ( 1st `  z ) ,  ( 2nd `  z )
>. )
140 df-ov 5877 . . . . . . . . . . . . . . 15  |-  ( ( 1st `  z ) (  Hom  `  B
) ( 2nd `  z
) )  =  ( (  Hom  `  B
) `  <. ( 1st `  z ) ,  ( 2nd `  z )
>. )
141138, 139, 1403eqtr3g 2351 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( (  Hom  `  A ) `  <. ( 1st `  z ) ,  ( 2nd `  z
) >. )  =  ( (  Hom  `  B
) `  <. ( 1st `  z ) ,  ( 2nd `  z )
>. ) )
142 1st2nd2 6175 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( ( Base `  A )  X.  ( Base `  A ) )  ->  z  =  <. ( 1st `  z ) ,  ( 2nd `  z
) >. )
143142adantl 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  z  =  <. ( 1st `  z ) ,  ( 2nd `  z
) >. )
144143fveq2d 5545 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( (  Hom  `  A ) `  z
)  =  ( (  Hom  `  A ) `  <. ( 1st `  z
) ,  ( 2nd `  z ) >. )
)
145143fveq2d 5545 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( (  Hom  `  B ) `  z
)  =  ( (  Hom  `  B ) `  <. ( 1st `  z
) ,  ( 2nd `  z ) >. )
)
146141, 144, 1453eqtr4d 2338 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( (  Hom  `  A ) `  z
)  =  ( (  Hom  `  B ) `  z ) )
147136, 146oveq12d 5892 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C )
( f `  ( 2nd `  z ) ) )  ^m  ( (  Hom  `  A ) `  z ) )  =  ( ( ( f `
 ( 1st `  z
) ) (  Hom  `  D ) ( f `
 ( 2nd `  z
) ) )  ^m  ( (  Hom  `  B
) `  z )
) )
148147ixpeq2dva 6847 . . . . . . . . . . 11  |-  ( (
ph  /\  f :
( Base `  A ) --> ( Base `  C )
)  ->  X_ z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) )  =  X_ z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  B ) `
 z ) ) )
1495homfeqbas 13615 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Base `  A
)  =  ( Base `  B ) )
150149, 149xpeq12d 4730 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( Base `  A
)  X.  ( Base `  A ) )  =  ( ( Base `  B
)  X.  ( Base `  B ) ) )
151150adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  f :
( Base `  A ) --> ( Base `  C )
)  ->  ( ( Base `  A )  X.  ( Base `  A
) )  =  ( ( Base `  B
)  X.  ( Base `  B ) ) )
152151ixpeq1d 6844 . . . . . . . . . . 11  |-  ( (
ph  /\  f :
( Base `  A ) --> ( Base `  C )
)  ->  X_ z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  B ) `
 z ) )  =  X_ z  e.  ( ( Base `  B
)  X.  ( Base `  B ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  B ) `
 z ) ) )
153148, 152eqtrd 2328 . . . . . . . . . 10  |-  ( (
ph  /\  f :
( Base `  A ) --> ( Base `  C )
)  ->  X_ z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) )  =  X_ z  e.  ( ( Base `  B
)  X.  ( Base `  B ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  B ) `
 z ) ) )
154153eleq2d 2363 . . . . . . . . 9  |-  ( (
ph  /\  f :
( Base `  A ) --> ( Base `  C )
)  ->  ( g  e.  X_ z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) )  <-> 
g  e.  X_ z  e.  ( ( Base `  B
)  X.  ( Base `  B ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  B ) `
 z ) ) ) )
155154pm5.32da 622 . . . . . . . 8  |-  ( ph  ->  ( ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ z  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) ) )  <->  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ z  e.  ( (
Base `  B )  X.  ( Base `  B
) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  B ) `
 z ) ) ) ) )
15610homfeqbas 13615 . . . . . . . . . 10  |-  ( ph  ->  ( Base `  C
)  =  ( Base `  D ) )
157149, 156feq23d 5402 . . . . . . . . 9  |-  ( ph  ->  ( f : (
Base `  A ) --> ( Base `  C )  <->  f : ( Base `  B
) --> ( Base `  D
) ) )
158157anbi1d 685 . . . . . . . 8  |-  ( ph  ->  ( ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ z  e.  ( (
Base `  B )  X.  ( Base `  B
) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  B ) `
 z ) ) )  <->  ( f : ( Base `  B
) --> ( Base `  D
)  /\  g  e.  X_ z  e.  ( (
Base `  B )  X.  ( Base `  B
) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  B ) `
 z ) ) ) ) )
159155, 158bitrd 244 . . . . . . 7  |-  ( ph  ->  ( ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ z  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) ) )  <->  ( f : ( Base `  B
) --> ( Base `  D
)  /\  g  e.  X_ z  e.  ( (
Base `  B )  X.  ( Base `  B
) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  B ) `
 z ) ) ) ) )
160149adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( Base `  A )
)  ->  ( Base `  A )  =  (
Base `  B )
)
161160raleqdv 2755 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( Base `  A )
)  ->  ( A. z  e.  ( Base `  A ) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) )  <->  A. z  e.  ( Base `  B ) A. m  e.  ( x
(  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B ) z ) ( ( x g z ) `  (
n ( <. x ,  y >. (comp `  B ) z ) m ) )  =  ( ( ( y g z ) `  n ) ( <.
( f `  x
) ,  ( f `
 y ) >.
(comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )
162160, 161raleqbidv 2761 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( Base `  A )
)  ->  ( A. y  e.  ( Base `  A ) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) )  <->  A. y  e.  ( Base `  B ) A. z  e.  ( Base `  B ) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )
163162anbi2d 684 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( Base `  A )
)  ->  ( (
( ( x g x ) `  (
( Id `  B
) `  x )
)  =  ( ( Id `  D ) `
 ( f `  x ) )  /\  A. y  e.  ( Base `  A ) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) )  <->  ( ( ( x g x ) `
 ( ( Id
`  B ) `  x ) )  =  ( ( Id `  D ) `  (
f `  x )
)  /\  A. y  e.  ( Base `  B
) A. z  e.  ( Base `  B
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) ) )
164149, 163raleqbidva 2763 . . . . . . 7  |-  ( ph  ->  ( A. x  e.  ( Base `  A
) ( ( ( x g x ) `
 ( ( Id
`  B ) `  x ) )  =  ( ( Id `  D ) `  (
f `  x )
)  /\  A. y  e.  ( Base `  A
) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) )  <->  A. x  e.  (
Base `  B )
( ( ( x g x ) `  ( ( Id `  B ) `  x
) )  =  ( ( Id `  D
) `  ( f `  x ) )  /\  A. y  e.  ( Base `  B ) A. z  e.  ( Base `  B
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) ) )
165159, 164anbi12d 691 . . . . . 6  |-  ( ph  ->  ( ( ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ z  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) ) )  /\  A. x  e.  ( Base `  A
) ( ( ( x g x ) `
 ( ( Id
`  B ) `  x ) )  =  ( ( Id `  D ) `  (
f `  x )
)  /\  A. y  e.  ( Base `  A
) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )  <->  ( (
f : ( Base `  B ) --> ( Base `  D )  /\  g  e.  X_ z  e.  ( ( Base `  B
)  X.  ( Base `  B ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  B ) `
 z ) ) )  /\  A. x  e.  ( Base `  B
) ( ( ( x g x ) `
 ( ( Id
`  B ) `  x ) )  =  ( ( Id `  D ) `  (
f `  x )
)  /\  A. y  e.  ( Base `  B
) A. z  e.  ( Base `  B
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) ) ) )
166126, 165bitrd 244 . . . . 5  |-  ( ph  ->  ( ( ( f : (