Metamath Proof Explorer

Theorem hof2fval

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

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 1 2 3 4 9 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 ) ) ) ) >. )
11 fvex 
 |-  ( Homf ` C ) e. _V
12 3 fvexi 
 |-  B e. _V
13 12 12 xpex 
 |-  ( B X. B ) e. _V
14 13 13 mpoex 
 |-  ( 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
15 11 14 op2ndd 
 |-  ( 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 ) ) ) ) >. -> ( 2nd ` M ) = ( 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 ) ) ) ) )
16 10 15 syl 
 |-  ( ph -> ( 2nd ` M ) = ( 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 ) ) ) ) )
17 simprr 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> y = <. Z , W >. )
18 17 fveq2d 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( 1st ` y ) = ( 1st ` <. Z , W >. ) )
19 op1stg 
 |-  ( ( Z e. B /\ W e. B ) -> ( 1st ` <. Z , W >. ) = Z )
20 7 8 19 syl2anc 
 |-  ( ph -> ( 1st ` <. Z , W >. ) = Z )
21 20 adantr 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( 1st ` <. Z , W >. ) = Z )
22 18 21 eqtrd 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( 1st ` y ) = Z )
23 simprl 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> x = <. X , Y >. )
24 23 fveq2d 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( 1st ` x ) = ( 1st ` <. X , Y >. ) )
25 op1stg 
 |-  ( ( X e. B /\ Y e. B ) -> ( 1st ` <. X , Y >. ) = X )
26 5 6 25 syl2anc 
 |-  ( ph -> ( 1st ` <. X , Y >. ) = X )
27 26 adantr 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( 1st ` <. X , Y >. ) = X )
28 24 27 eqtrd 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( 1st ` x ) = X )
29 22 28 oveq12d 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( ( 1st ` y ) H ( 1st ` x ) ) = ( Z H X ) )
30 23 fveq2d 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( 2nd ` x ) = ( 2nd ` <. X , Y >. ) )
31 op2ndg 
 |-  ( ( X e. B /\ Y e. B ) -> ( 2nd ` <. X , Y >. ) = Y )
32 5 6 31 syl2anc 
 |-  ( ph -> ( 2nd ` <. X , Y >. ) = Y )
33 32 adantr 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( 2nd ` <. X , Y >. ) = Y )
34 30 33 eqtrd 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( 2nd ` x ) = Y )
35 17 fveq2d 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( 2nd ` y ) = ( 2nd ` <. Z , W >. ) )
36 op2ndg 
 |-  ( ( Z e. B /\ W e. B ) -> ( 2nd ` <. Z , W >. ) = W )
37 7 8 36 syl2anc 
 |-  ( ph -> ( 2nd ` <. Z , W >. ) = W )
38 37 adantr 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( 2nd ` <. Z , W >. ) = W )
39 35 38 eqtrd 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( 2nd ` y ) = W )
40 34 39 oveq12d 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( ( 2nd ` x ) H ( 2nd ` y ) ) = ( Y H W ) )
41 23 fveq2d 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( H ` x ) = ( H ` <. X , Y >. ) )
42 df-ov 
 |-  ( X H Y ) = ( H ` <. X , Y >. )
43 41 42 eqtr4di 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( H ` x ) = ( X H Y ) )
44 22 28 opeq12d 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> <. ( 1st ` y ) , ( 1st ` x ) >. = <. Z , X >. )
45 44 39 oveq12d 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( <. ( 1st ` y ) , ( 1st ` x ) >. .x. ( 2nd ` y ) ) = ( <. Z , X >. .x. W ) )
46 23 39 oveq12d 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( x .x. ( 2nd ` y ) ) = ( <. X , Y >. .x. W ) )
47 46 oveqd 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( g ( x .x. ( 2nd ` y ) ) h ) = ( g ( <. X , Y >. .x. W ) h ) )
48 eqidd 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> f = f )
49 45 47 48 oveq123d 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( ( g ( x .x. ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. .x. ( 2nd ` y ) ) f ) = ( ( g ( <. X , Y >. .x. W ) h ) ( <. Z , X >. .x. W ) f ) )
50 43 49 mpteq12dv 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( h e. ( H ` x ) |-> ( ( g ( x .x. ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. .x. ( 2nd ` y ) ) f ) ) = ( h e. ( X H Y ) |-> ( ( g ( <. X , Y >. .x. W ) h ) ( <. Z , X >. .x. W ) f ) ) )
51 29 40 50 mpoeq123dv 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = <. Z , W >. ) ) -> ( 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 ) ) ) = ( 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 ) ) ) )
52 5 6 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( B X. B ) )
53 7 8 opelxpd 
 |-  ( ph -> <. Z , W >. e. ( B X. B ) )
54 ovex 
 |-  ( Z H X ) e. _V
55 ovex 
 |-  ( Y H W ) e. _V
56 54 55 mpoex 
 |-  ( 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 ) ) ) e. _V
57 56 a1i 
 |-  ( ph -> ( 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 ) ) ) e. _V )
58 16 51 52 53 57 ovmpod 
 |-  ( 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 ) ) ) )