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

Metamath Proof Explorer

Theorem comfval

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 )
comfval.f 
|- ( ph -> F e. ( X H Y ) )
comfval.g 
|- ( ph -> G e. ( Y H Z ) )
Assertion comfval 
|- ( ph -> ( G ( <. X , Y >. O Z ) F ) = ( 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 comfval.f 
 |-  ( ph -> F e. ( X H Y ) )
9 comfval.g 
 |-  ( ph -> G e. ( Y H Z ) )
10 1 2 3 4 5 6 7 comffval 
 |-  ( ph -> ( <. X , Y >. O Z ) = ( g e. ( Y H Z ) , f e. ( X H Y ) |-> ( g ( <. X , Y >. .x. Z ) f ) ) )
11 oveq12 
 |-  ( ( g = G /\ f = F ) -> ( g ( <. X , Y >. .x. Z ) f ) = ( G ( <. X , Y >. .x. Z ) F ) )
12 11 adantl 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( g ( <. X , Y >. .x. Z ) f ) = ( G ( <. X , Y >. .x. Z ) F ) )
13 ovexd 
 |-  ( ph -> ( G ( <. X , Y >. .x. Z ) F ) e. _V )
14 10 12 9 8 13 ovmpod 
 |-  ( ph -> ( G ( <. X , Y >. O Z ) F ) = ( G ( <. X , Y >. .x. Z ) F ) )