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

Theorem hofval 14075
Description: Value of the Hom functor, which is a bifunctor (a functor of two arguments), contravariant in the first argument and covariant in the second, from  (oppCat `  C )  X.  C to  SetCat, whose object part is the hom-function 
Hom, and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 15-Jan-2017.)
Hypotheses
Ref Expression
hofval.m  |-  M  =  (HomF
`  C )
hofval.c  |-  ( ph  ->  C  e.  Cat )
hofval.b  |-  B  =  ( Base `  C
)
hofval.h  |-  H  =  (  Hom  `  C
)
hofval.o  |-  .x.  =  (comp `  C )
Assertion
Ref Expression
hofval  |-  ( ph  ->  M  =  <. (  Homf  `  C ) ,  ( x  e.  ( B  X.  B ) ,  y  e.  ( B  X.  B )  |->  ( f  e.  ( ( 1st `  y ) H ( 1st `  x
) ) ,  g  e.  ( ( 2nd `  x ) H ( 2nd `  y ) )  |->  ( h  e.  ( H `  x
)  |->  ( ( g ( x  .x.  ( 2nd `  y ) ) h ) ( <.
( 1st `  y
) ,  ( 1st `  x ) >.  .x.  ( 2nd `  y ) ) f ) ) ) ) >. )
Distinct variable groups:    f, g, h, x, y, B    ph, f,
g, h, x, y    C, f, g, h, x, y    f, H, g, h, x, y    .x. , f,
g, h, x, y
Allowed substitution hints:    M( x, y, f, g, h)

Proof of Theorem hofval
Dummy variables  b 
c are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hofval.m . 2  |-  M  =  (HomF
`  C )
2 df-hof 14073 . . . 4  |- HomF  =  ( c  e.  Cat  |->  <. (  Homf  `  c ) ,  [_ ( Base `  c )  /  b ]_ ( x  e.  ( b  X.  b ) ,  y  e.  ( b  X.  b ) 
|->  ( f  e.  ( ( 1st `  y
) (  Hom  `  c
) ( 1st `  x
) ) ,  g  e.  ( ( 2nd `  x ) (  Hom  `  c ) ( 2nd `  y ) )  |->  ( h  e.  ( (  Hom  `  c ) `  x )  |->  ( ( g ( x (comp `  c ) ( 2nd `  y ) ) h ) ( <. ( 1st `  y ) ,  ( 1st `  x
) >. (comp `  c
) ( 2nd `  y
) ) f ) ) ) ) >.
)
32a1i 10 . . 3  |-  ( ph  -> HomF  =  ( c  e.  Cat  |->  <. (  Homf 
`  c ) , 
[_ ( Base `  c
)  /  b ]_ ( x  e.  (
b  X.  b ) ,  y  e.  ( b  X.  b ) 
|->  ( f  e.  ( ( 1st `  y
) (  Hom  `  c
) ( 1st `  x
) ) ,  g  e.  ( ( 2nd `  x ) (  Hom  `  c ) ( 2nd `  y ) )  |->  ( h  e.  ( (  Hom  `  c ) `  x )  |->  ( ( g ( x (comp `  c ) ( 2nd `  y ) ) h ) ( <. ( 1st `  y ) ,  ( 1st `  x
) >. (comp `  c
) ( 2nd `  y
) ) f ) ) ) ) >.
) )
4 simpr 447 . . . . 5  |-  ( (
ph  /\  c  =  C )  ->  c  =  C )
54fveq2d 5567 . . . 4  |-  ( (
ph  /\  c  =  C )  ->  (  Homf  `  c )  =  (  Homf 
`  C ) )
6 fvex 5577 . . . . . 6  |-  ( Base `  c )  e.  _V
76a1i 10 . . . . 5  |-  ( (
ph  /\  c  =  C )  ->  ( Base `  c )  e. 
_V )
84fveq2d 5567 . . . . . 6  |-  ( (
ph  /\  c  =  C )  ->  ( Base `  c )  =  ( Base `  C
) )
9 hofval.b . . . . . 6  |-  B  =  ( Base `  C
)
108, 9syl6eqr 2366 . . . . 5  |-  ( (
ph  /\  c  =  C )  ->  ( Base `  c )  =  B )
11 simpr 447 . . . . . . 7  |-  ( ( ( ph  /\  c  =  C )  /\  b  =  B )  ->  b  =  B )
1211, 11xpeq12d 4751 . . . . . 6  |-  ( ( ( ph  /\  c  =  C )  /\  b  =  B )  ->  (
b  X.  b )  =  ( B  X.  B ) )
13 simplr 731 . . . . . . . . . 10  |-  ( ( ( ph  /\  c  =  C )  /\  b  =  B )  ->  c  =  C )
1413fveq2d 5567 . . . . . . . . 9  |-  ( ( ( ph  /\  c  =  C )  /\  b  =  B )  ->  (  Hom  `  c )  =  (  Hom  `  C
) )
15 hofval.h . . . . . . . . 9  |-  H  =  (  Hom  `  C
)
1614, 15syl6eqr 2366 . . . . . . . 8  |-  ( ( ( ph  /\  c  =  C )  /\  b  =  B )  ->  (  Hom  `  c )  =  H )
1716oveqd 5917 . . . . . . 7  |-  ( ( ( ph  /\  c  =  C )  /\  b  =  B )  ->  (
( 1st `  y
) (  Hom  `  c
) ( 1st `  x
) )  =  ( ( 1st `  y
) H ( 1st `  x ) ) )
1816oveqd 5917 . . . . . . 7  |-  ( ( ( ph  /\  c  =  C )  /\  b  =  B )  ->  (
( 2nd `  x
) (  Hom  `  c
) ( 2nd `  y
) )  =  ( ( 2nd `  x
) H ( 2nd `  y ) ) )
1916fveq1d 5565 . . . . . . . 8  |-  ( ( ( ph  /\  c  =  C )  /\  b  =  B )  ->  (
(  Hom  `  c ) `
 x )  =  ( H `  x
) )
2013fveq2d 5567 . . . . . . . . . . 11  |-  ( ( ( ph  /\  c  =  C )  /\  b  =  B )  ->  (comp `  c )  =  (comp `  C ) )
21 hofval.o . . . . . . . . . . 11  |-  .x.  =  (comp `  C )
2220, 21syl6eqr 2366 . . . . . . . . . 10  |-  ( ( ( ph  /\  c  =  C )  /\  b  =  B )  ->  (comp `  c )  =  .x.  )
2322oveqd 5917 . . . . . . . . 9  |-  ( ( ( ph  /\  c  =  C )  /\  b  =  B )  ->  ( <. ( 1st `  y
) ,  ( 1st `  x ) >. (comp `  c ) ( 2nd `  y ) )  =  ( <. ( 1st `  y
) ,  ( 1st `  x ) >.  .x.  ( 2nd `  y ) ) )
2422oveqd 5917 . . . . . . . . . 10  |-  ( ( ( ph  /\  c  =  C )  /\  b  =  B )  ->  (
x (comp `  c
) ( 2nd `  y
) )  =  ( x  .x.  ( 2nd `  y ) ) )
2524oveqd 5917 . . . . . . . . 9  |-  ( ( ( ph  /\  c  =  C )  /\  b  =  B )  ->  (
g ( x (comp `  c ) ( 2nd `  y ) ) h )  =  ( g ( x  .x.  ( 2nd `  y ) ) h ) )
26 eqidd 2317 . . . . . . . . 9  |-  ( ( ( ph  /\  c  =  C )  /\  b  =  B )  ->  f  =  f )
2723, 25, 26oveq123d 5921 . . . . . . . 8  |-  ( ( ( ph  /\  c  =  C )  /\  b  =  B )  ->  (
( g ( x (comp `  c )
( 2nd `  y
) ) h ) ( <. ( 1st `  y
) ,  ( 1st `  x ) >. (comp `  c ) ( 2nd `  y ) ) f )  =  ( ( g ( x  .x.  ( 2nd `  y ) ) h ) (
<. ( 1st `  y
) ,  ( 1st `  x ) >.  .x.  ( 2nd `  y ) ) f ) )
2819, 27mpteq12dv 4135 . . . . . . 7  |-  ( ( ( ph  /\  c  =  C )  /\  b  =  B )  ->  (
h  e.  ( (  Hom  `  c ) `  x )  |->  ( ( g ( x (comp `  c ) ( 2nd `  y ) ) h ) ( <. ( 1st `  y ) ,  ( 1st `  x
) >. (comp `  c
) ( 2nd `  y
) ) f ) )  =  ( h  e.  ( H `  x )  |->  ( ( g ( x  .x.  ( 2nd `  y ) ) h ) (
<. ( 1st `  y
) ,  ( 1st `  x ) >.  .x.  ( 2nd `  y ) ) f ) ) )
2917, 18, 28mpt2eq123dv 5952 . . . . . 6  |-  ( ( ( ph  /\  c  =  C )  /\  b  =  B )  ->  (
f  e.  ( ( 1st `  y ) (  Hom  `  c
) ( 1st `  x
) ) ,  g  e.  ( ( 2nd `  x ) (  Hom  `  c ) ( 2nd `  y ) )  |->  ( h  e.  ( (  Hom  `  c ) `  x )  |->  ( ( g ( x (comp `  c ) ( 2nd `  y ) ) h ) ( <. ( 1st `  y ) ,  ( 1st `  x
) >. (comp `  c
) ( 2nd `  y
) ) f ) ) )  =  ( f  e.  ( ( 1st `  y ) H ( 1st `  x
) ) ,  g  e.  ( ( 2nd `  x ) H ( 2nd `  y ) )  |->  ( h  e.  ( H `  x
)  |->  ( ( g ( x  .x.  ( 2nd `  y ) ) h ) ( <.
( 1st `  y
) ,  ( 1st `  x ) >.  .x.  ( 2nd `  y ) ) f ) ) ) )
3012, 12, 29mpt2eq123dv 5952 . . . . 5  |-  ( ( ( ph  /\  c  =  C )  /\  b  =  B )  ->  (
x  e.  ( b  X.  b ) ,  y  e.  ( b  X.  b )  |->  ( f  e.  ( ( 1st `  y ) (  Hom  `  c
) ( 1st `  x
) ) ,  g  e.  ( ( 2nd `  x ) (  Hom  `  c ) ( 2nd `  y ) )  |->  ( h  e.  ( (  Hom  `  c ) `  x )  |->  ( ( g ( x (comp `  c ) ( 2nd `  y ) ) h ) ( <. ( 1st `  y ) ,  ( 1st `  x
) >. (comp `  c
) ( 2nd `  y
) ) f ) ) ) )  =  ( x  e.  ( B  X.  B ) ,  y  e.  ( B  X.  B ) 
|->  ( f  e.  ( ( 1st `  y
) H ( 1st `  x ) ) ,  g  e.  ( ( 2nd `  x ) H ( 2nd `  y
) )  |->  ( h  e.  ( H `  x )  |->  ( ( g ( x  .x.  ( 2nd `  y ) ) h ) (
<. ( 1st `  y
) ,  ( 1st `  x ) >.  .x.  ( 2nd `  y ) ) f ) ) ) ) )
317, 10, 30csbied2 3158 . . . 4  |-  ( (
ph  /\  c  =  C )  ->  [_ ( Base `  c )  / 
b ]_ ( x  e.  ( b  X.  b
) ,  y  e.  ( b  X.  b
)  |->  ( f  e.  ( ( 1st `  y
) (  Hom  `  c
) ( 1st `  x
) ) ,  g  e.  ( ( 2nd `  x ) (  Hom  `  c ) ( 2nd `  y ) )  |->  ( h  e.  ( (  Hom  `  c ) `  x )  |->  ( ( g ( x (comp `  c ) ( 2nd `  y ) ) h ) ( <. ( 1st `  y ) ,  ( 1st `  x
) >. (comp `  c
) ( 2nd `  y
) ) f ) ) ) )  =  ( x  e.  ( B  X.  B ) ,  y  e.  ( B  X.  B ) 
|->  ( f  e.  ( ( 1st `  y
) H ( 1st `  x ) ) ,  g  e.  ( ( 2nd `  x ) H ( 2nd `  y
) )  |->  ( h  e.  ( H `  x )  |->  ( ( g ( x  .x.  ( 2nd `  y ) ) h ) (
<. ( 1st `  y
) ,  ( 1st `  x ) >.  .x.  ( 2nd `  y ) ) f ) ) ) ) )
325, 31opeq12d 3841 . . 3  |-  ( (
ph  /\  c  =  C )  ->  <. (  Homf  `  c ) ,  [_ ( Base `  c )  /  b ]_ (
x  e.  ( b  X.  b ) ,  y  e.  ( b  X.  b )  |->  ( f  e.  ( ( 1st `  y ) (  Hom  `  c
) ( 1st `  x
) ) ,  g  e.  ( ( 2nd `  x ) (  Hom  `  c ) ( 2nd `  y ) )  |->  ( h  e.  ( (  Hom  `  c ) `  x )  |->  ( ( g ( x (comp `  c ) ( 2nd `  y ) ) h ) ( <. ( 1st `  y ) ,  ( 1st `  x
) >. (comp `  c
) ( 2nd `  y
) ) f ) ) ) ) >.  =  <. (  Homf  `  C ) ,  ( x  e.  ( B  X.  B
) ,  y  e.  ( B  X.  B
)  |->  ( f  e.  ( ( 1st `  y
) H ( 1st `  x ) ) ,  g  e.  ( ( 2nd `  x ) H ( 2nd `  y
) )  |->  ( h  e.  ( H `  x )  |->  ( ( g ( x  .x.  ( 2nd `  y ) ) h ) (
<. ( 1st `  y
) ,  ( 1st `  x ) >.  .x.  ( 2nd `  y ) ) f ) ) ) ) >. )
33 hofval.c . . 3  |-  ( ph  ->  C  e.  Cat )
34 opex 4274 . . . 4  |-  <. (  Homf  `  C ) ,  ( x  e.  ( B  X.  B ) ,  y  e.  ( B  X.  B )  |->  ( f  e.  ( ( 1st `  y ) H ( 1st `  x
) ) ,  g  e.  ( ( 2nd `  x ) H ( 2nd `  y ) )  |->  ( h  e.  ( H `  x
)  |->  ( ( g ( x  .x.  ( 2nd `  y ) ) h ) ( <.
( 1st `  y
) ,  ( 1st `  x ) >.  .x.  ( 2nd `  y ) ) f ) ) ) ) >.  e.  _V
3534a1i 10 . . 3  |-  ( ph  -> 
<. (  Homf 
`  C ) ,  ( x  e.  ( B  X.  B ) ,  y  e.  ( B  X.  B ) 
|->  ( f  e.  ( ( 1st `  y
) H ( 1st `  x ) ) ,  g  e.  ( ( 2nd `  x ) H ( 2nd `  y
) )  |->  ( h  e.  ( H `  x )  |->  ( ( g ( x  .x.  ( 2nd `  y ) ) h ) (
<. ( 1st `  y
) ,  ( 1st `  x ) >.  .x.  ( 2nd `  y ) ) f ) ) ) ) >.  e.  _V )
363, 32, 33, 35fvmptd 5644 . 2  |-  ( ph  ->  (HomF
`  C )  = 
<. (  Homf 
`  C ) ,  ( x  e.  ( B  X.  B ) ,  y  e.  ( B  X.  B ) 
|->  ( f  e.  ( ( 1st `  y
) H ( 1st `  x ) ) ,  g  e.  ( ( 2nd `  x ) H ( 2nd `  y
) )  |->  ( h  e.  ( H `  x )  |->  ( ( g ( x  .x.  ( 2nd `  y ) ) h ) (
<. ( 1st `  y
) ,  ( 1st `  x ) >.  .x.  ( 2nd `  y ) ) f ) ) ) ) >. )
371, 36syl5eq 2360 1  |-  ( ph  ->  M  =  <. (  Homf  `  C ) ,  ( x  e.  ( B  X.  B ) ,  y  e.  ( B  X.  B )  |->  ( f  e.  ( ( 1st `  y ) H ( 1st `  x
) ) ,  g  e.  ( ( 2nd `  x ) H ( 2nd `  y ) )  |->  ( h  e.  ( H `  x
)  |->  ( ( g ( x  .x.  ( 2nd `  y ) ) h ) ( <.
( 1st `  y
) ,  ( 1st `  x ) >.  .x.  ( 2nd `  y ) ) f ) ) ) ) >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1633    e. wcel 1701   _Vcvv 2822   [_csb 3115   <.cop 3677    e. cmpt 4114    X. cxp 4724   ` cfv 5292  (class class class)co 5900    e. cmpt2 5902   1stc1st 6162   2ndc2nd 6163   Basecbs 13195    Hom chom 13266  compcco 13267   Catccat 13615    Homf chomf 13617  HomFchof 14071
This theorem is referenced by:  hof1fval  14076  hof2fval  14078  hofcl  14082  hofpropd  14090
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-opab 4115  df-mpt 4116  df-id 4346  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-iota 5256  df-fun 5294  df-fv 5300  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-hof 14073
  Copyright terms: Public domain W3C validator