Metamath Proof Explorer

Theorem comffval

Description: Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses comfffval.o 
|- O = ( comf ` C )
comfffval.b 
|- B = ( Base ` C )
comfffval.h 
|- H = ( Hom ` C )
comfffval.x 
|- .x. = ( comp ` C )
comffval.x 
|- ( ph -> X e. B )
comffval.y 
|- ( ph -> Y e. B )
comffval.z 
|- ( ph -> Z e. B )
Assertion comffval 
|- ( ph -> ( <. X , Y >. O Z ) = ( g e. ( Y H Z ) , f e. ( X H Y ) |-> ( g ( <. X , Y >. .x. Z ) f ) ) )

Proof

Step Hyp Ref Expression
1 comfffval.o 
 |-  O = ( comf ` C )
2 comfffval.b 
 |-  B = ( Base ` C )
3 comfffval.h 
 |-  H = ( Hom ` C )
4 comfffval.x 
 |-  .x. = ( comp ` C )
5 comffval.x 
 |-  ( ph -> X e. B )
6 comffval.y 
 |-  ( ph -> Y e. B )
7 comffval.z 
 |-  ( ph -> Z e. B )
8 1 2 3 4 comfffval 
 |-  O = ( x e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` x ) H z ) , f e. ( H ` x ) |-> ( g ( x .x. z ) f ) ) )
9 8 a1i 
 |-  ( ph -> O = ( x e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` x ) H z ) , f e. ( H ` x ) |-> ( g ( x .x. z ) f ) ) ) )
10 simprl 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ z = Z ) ) -> x = <. X , Y >. )
11 10 fveq2d 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ z = Z ) ) -> ( 2nd ` x ) = ( 2nd ` <. X , Y >. ) )
12 op2ndg 
 |-  ( ( X e. B /\ Y e. B ) -> ( 2nd ` <. X , Y >. ) = Y )
13 5 6 12 syl2anc 
 |-  ( ph -> ( 2nd ` <. X , Y >. ) = Y )
14 13 adantr 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ z = Z ) ) -> ( 2nd ` <. X , Y >. ) = Y )
15 11 14 eqtrd 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ z = Z ) ) -> ( 2nd ` x ) = Y )
16 simprr 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ z = Z ) ) -> z = Z )
17 15 16 oveq12d 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ z = Z ) ) -> ( ( 2nd ` x ) H z ) = ( Y H Z ) )
18 10 fveq2d 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ z = Z ) ) -> ( H ` x ) = ( H ` <. X , Y >. ) )
19 df-ov 
 |-  ( X H Y ) = ( H ` <. X , Y >. )
20 18 19 eqtr4di 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ z = Z ) ) -> ( H ` x ) = ( X H Y ) )
21 10 16 oveq12d 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ z = Z ) ) -> ( x .x. z ) = ( <. X , Y >. .x. Z ) )
22 21 oveqd 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ z = Z ) ) -> ( g ( x .x. z ) f ) = ( g ( <. X , Y >. .x. Z ) f ) )
23 17 20 22 mpoeq123dv 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ z = Z ) ) -> ( g e. ( ( 2nd ` x ) H z ) , f e. ( H ` x ) |-> ( g ( x .x. z ) f ) ) = ( g e. ( Y H Z ) , f e. ( X H Y ) |-> ( g ( <. X , Y >. .x. Z ) f ) ) )
24 5 6 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( B X. B ) )
25 ovex 
 |-  ( Y H Z ) e. _V
26 ovex 
 |-  ( X H Y ) e. _V
27 25 26 mpoex 
 |-  ( g e. ( Y H Z ) , f e. ( X H Y ) |-> ( g ( <. X , Y >. .x. Z ) f ) ) e. _V
28 27 a1i 
 |-  ( ph -> ( g e. ( Y H Z ) , f e. ( X H Y ) |-> ( g ( <. X , Y >. .x. Z ) f ) ) e. _V )
29 9 23 24 7 28 ovmpod 
 |-  ( ph -> ( <. X , Y >. O Z ) = ( g e. ( Y H Z ) , f e. ( X H Y ) |-> ( g ( <. X , Y >. .x. Z ) f ) ) )