Metamath Proof Explorer

Theorem hofval

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

Ref Expression
Hypotheses 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 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 ) ) ) ) >. )

Proof

Step Hyp Ref Expression
1 hofval.m 
 |-  M = ( HomF ` C )
2 hofval.c 
 |-  ( ph -> C e. Cat )
3 hofval.b 
 |-  B = ( Base ` C )
4 hofval.h 
 |-  H = ( Hom ` C )
5 hofval.o 
 |-  .x. = ( comp ` C )
6 df-hof 
 |-  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 ) ) ) ) >. )
7 simpr 
 |-  ( ( ph /\ c = C ) -> c = C )
8 7 fveq2d 
 |-  ( ( ph /\ c = C ) -> ( Homf ` c ) = ( Homf ` C ) )
9 fvexd 
 |-  ( ( ph /\ c = C ) -> ( Base ` c ) e. _V )
10 7 fveq2d 
 |-  ( ( ph /\ c = C ) -> ( Base ` c ) = ( Base ` C ) )
11 10 3 eqtr4di 
 |-  ( ( ph /\ c = C ) -> ( Base ` c ) = B )
12 simpr 
 |-  ( ( ( ph /\ c = C ) /\ b = B ) -> b = B )
13 12 sqxpeqd 
 |-  ( ( ( ph /\ c = C ) /\ b = B ) -> ( b X. b ) = ( B X. B ) )
14 simplr 
 |-  ( ( ( ph /\ c = C ) /\ b = B ) -> c = C )
15 14 fveq2d 
 |-  ( ( ( ph /\ c = C ) /\ b = B ) -> ( Hom ` c ) = ( Hom ` C ) )
16 15 4 eqtr4di 
 |-  ( ( ( ph /\ c = C ) /\ b = B ) -> ( Hom ` c ) = H )
17 16 oveqd 
 |-  ( ( ( ph /\ c = C ) /\ b = B ) -> ( ( 1st ` y ) ( Hom ` c ) ( 1st ` x ) ) = ( ( 1st ` y ) H ( 1st ` x ) ) )
18 16 oveqd 
 |-  ( ( ( ph /\ c = C ) /\ b = B ) -> ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) ) = ( ( 2nd ` x ) H ( 2nd ` y ) ) )
19 16 fveq1d 
 |-  ( ( ( ph /\ c = C ) /\ b = B ) -> ( ( Hom ` c ) ` x ) = ( H ` x ) )
20 14 fveq2d 
 |-  ( ( ( ph /\ c = C ) /\ b = B ) -> ( comp ` c ) = ( comp ` C ) )
21 20 5 eqtr4di 
 |-  ( ( ( ph /\ c = C ) /\ b = B ) -> ( comp ` c ) = .x. )
22 21 oveqd 
 |-  ( ( ( ph /\ c = C ) /\ b = B ) -> ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` c ) ( 2nd ` y ) ) = ( <. ( 1st ` y ) , ( 1st ` x ) >. .x. ( 2nd ` y ) ) )
23 21 oveqd 
 |-  ( ( ( ph /\ c = C ) /\ b = B ) -> ( x ( comp ` c ) ( 2nd ` y ) ) = ( x .x. ( 2nd ` y ) ) )
24 23 oveqd 
 |-  ( ( ( ph /\ c = C ) /\ b = B ) -> ( g ( x ( comp ` c ) ( 2nd ` y ) ) h ) = ( g ( x .x. ( 2nd ` y ) ) h ) )
25 eqidd 
 |-  ( ( ( ph /\ c = C ) /\ b = B ) -> f = f )
26 22 24 25 oveq123d 
 |-  ( ( ( 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 ) )
27 19 26 mpteq12dv 
 |-  ( ( ( 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 ) ) )
28 17 18 27 mpoeq123dv 
 |-  ( ( ( 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 ) ) ) )
29 13 13 28 mpoeq123dv 
 |-  ( ( ( 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 ) ) ) ) )
30 9 11 29 csbied2 
 |-  ( ( 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 ) ) ) ) )
31 8 30 opeq12d 
 |-  ( ( 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 ) ) ) ) >. )
32 opex 
 |-  <. ( 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
33 32 a1i 
 |-  ( 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 )
34 6 31 2 33 fvmptd2 
 |-  ( 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 ) ) ) ) >. )
35 1 34 syl5eq 
 |-  ( 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 ) ) ) ) >. )