Metamath Proof Explorer

Theorem hof2val

Description: The morphism part of the Hom functor, for morphisms <. f , g >. : <. X , Y >. --> <. Z , W >. (which since the first argument is contravariant means morphisms f : Z --> X and g : Y --> W ), yields a function (a morphism of SetCat ) mapping h : X --> Y to g o. h o. f : Z --> W . (Contributed by Mario Carneiro, 15-Jan-2017)

Ref Expression
Hypotheses hofval.m 
|- M = ( HomF ` C )
hofval.c 
|- ( ph -> C e. Cat )
hof1.b 
|- B = ( Base ` C )
hof1.h 
|- H = ( Hom ` C )
hof1.x 
|- ( ph -> X e. B )
hof1.y 
|- ( ph -> Y e. B )
hof2.z 
|- ( ph -> Z e. B )
hof2.w 
|- ( ph -> W e. B )
hof2.o 
|- .x. = ( comp ` C )
hof2.f 
|- ( ph -> F e. ( Z H X ) )
hof2.g 
|- ( ph -> G e. ( Y H W ) )
Assertion hof2val 
|- ( ph -> ( F ( <. X , Y >. ( 2nd ` M ) <. Z , W >. ) G ) = ( h e. ( X H Y ) |-> ( ( G ( <. X , Y >. .x. W ) h ) ( <. Z , X >. .x. W ) F ) ) )

Proof

Step Hyp Ref Expression
1 hofval.m 
 |-  M = ( HomF ` C )
2 hofval.c 
 |-  ( ph -> C e. Cat )
3 hof1.b 
 |-  B = ( Base ` C )
4 hof1.h 
 |-  H = ( Hom ` C )
5 hof1.x 
 |-  ( ph -> X e. B )
6 hof1.y 
 |-  ( ph -> Y e. B )
7 hof2.z 
 |-  ( ph -> Z e. B )
8 hof2.w 
 |-  ( ph -> W e. B )
9 hof2.o 
 |-  .x. = ( comp ` C )
10 hof2.f 
 |-  ( ph -> F e. ( Z H X ) )
11 hof2.g 
 |-  ( ph -> G e. ( Y H W ) )
12 1 2 3 4 5 6 7 8 9 hof2fval 
 |-  ( ph -> ( <. X , Y >. ( 2nd ` M ) <. Z , W >. ) = ( f e. ( Z H X ) , g e. ( Y H W ) |-> ( h e. ( X H Y ) |-> ( ( g ( <. X , Y >. .x. W ) h ) ( <. Z , X >. .x. W ) f ) ) ) )
13 simplrr 
 |-  ( ( ( ph /\ ( f = F /\ g = G ) ) /\ h e. ( X H Y ) ) -> g = G )
14 13 oveq1d 
 |-  ( ( ( ph /\ ( f = F /\ g = G ) ) /\ h e. ( X H Y ) ) -> ( g ( <. X , Y >. .x. W ) h ) = ( G ( <. X , Y >. .x. W ) h ) )
15 simplrl 
 |-  ( ( ( ph /\ ( f = F /\ g = G ) ) /\ h e. ( X H Y ) ) -> f = F )
16 14 15 oveq12d 
 |-  ( ( ( ph /\ ( f = F /\ g = G ) ) /\ h e. ( X H Y ) ) -> ( ( g ( <. X , Y >. .x. W ) h ) ( <. Z , X >. .x. W ) f ) = ( ( G ( <. X , Y >. .x. W ) h ) ( <. Z , X >. .x. W ) F ) )
17 16 mpteq2dva 
 |-  ( ( ph /\ ( f = F /\ g = G ) ) -> ( h e. ( X H Y ) |-> ( ( g ( <. X , Y >. .x. W ) h ) ( <. Z , X >. .x. W ) f ) ) = ( h e. ( X H Y ) |-> ( ( G ( <. X , Y >. .x. W ) h ) ( <. Z , X >. .x. W ) F ) ) )
18 ovex 
 |-  ( X H Y ) e. _V
19 18 mptex 
 |-  ( h e. ( X H Y ) |-> ( ( G ( <. X , Y >. .x. W ) h ) ( <. Z , X >. .x. W ) F ) ) e. _V
20 19 a1i 
 |-  ( ph -> ( h e. ( X H Y ) |-> ( ( G ( <. X , Y >. .x. W ) h ) ( <. Z , X >. .x. W ) F ) ) e. _V )
21 12 17 10 11 20 ovmpod 
 |-  ( ph -> ( F ( <. X , Y >. ( 2nd ` M ) <. Z , W >. ) G ) = ( h e. ( X H Y ) |-> ( ( G ( <. X , Y >. .x. W ) h ) ( <. Z , X >. .x. W ) F ) ) )