This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem comffval2

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

Ref Expression
Hypotheses comfffval2.o 
|- O = ( comf ` C )
comfffval2.b 
|- B = ( Base ` C )
comfffval2.h 
|- H = ( Homf ` C )
comfffval2.x 
|- .x. = ( comp ` C )
comffval2.x 
|- ( ph -> X e. B )
comffval2.y 
|- ( ph -> Y e. B )
comffval2.z 
|- ( ph -> Z e. B )
Assertion comffval2 
|- ( 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 comfffval2.o 
 |-  O = ( comf ` C )
2 comfffval2.b 
 |-  B = ( Base ` C )
3 comfffval2.h 
 |-  H = ( Homf ` C )
4 comfffval2.x 
 |-  .x. = ( comp ` C )
5 comffval2.x 
 |-  ( ph -> X e. B )
6 comffval2.y 
 |-  ( ph -> Y e. B )
7 comffval2.z 
 |-  ( ph -> Z e. B )
8 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
9 1 2 8 4 5 6 7 comffval 
 |-  ( ph -> ( <. X , Y >. O Z ) = ( g e. ( Y ( Hom ` C ) Z ) , f e. ( X ( Hom ` C ) Y ) |-> ( g ( <. X , Y >. .x. Z ) f ) ) )
10 3 2 8 6 7 homfval 
 |-  ( ph -> ( Y H Z ) = ( Y ( Hom ` C ) Z ) )
11 3 2 8 5 6 homfval 
 |-  ( ph -> ( X H Y ) = ( X ( Hom ` C ) Y ) )
12 eqidd 
 |-  ( ph -> ( g ( <. X , Y >. .x. Z ) f ) = ( g ( <. X , Y >. .x. Z ) f ) )
13 10 11 12 mpoeq123dv 
 |-  ( ph -> ( g e. ( Y H Z ) , f e. ( X H Y ) |-> ( g ( <. X , Y >. .x. Z ) f ) ) = ( g e. ( Y ( Hom ` C ) Z ) , f e. ( X ( Hom ` C ) Y ) |-> ( g ( <. X , Y >. .x. Z ) f ) ) )
14 9 13 eqtr4d 
 |-  ( ph -> ( <. X , Y >. O Z ) = ( g e. ( Y H Z ) , f e. ( X H Y ) |-> ( g ( <. X , Y >. .x. Z ) f ) ) )