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

Metamath Proof Explorer

Theorem comfval2

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 )
comfval2.f 
|- ( ph -> F e. ( X H Y ) )
comfval2.g 
|- ( ph -> G e. ( Y H Z ) )
Assertion comfval2 
|- ( ph -> ( G ( <. X , Y >. O Z ) F ) = ( 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 comfval2.f 
 |-  ( ph -> F e. ( X H Y ) )
9 comfval2.g 
 |-  ( ph -> G e. ( Y H Z ) )
10 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
11 3 2 10 5 6 homfval 
 |-  ( ph -> ( X H Y ) = ( X ( Hom ` C ) Y ) )
12 8 11 eleqtrd 
 |-  ( ph -> F e. ( X ( Hom ` C ) Y ) )
13 3 2 10 6 7 homfval 
 |-  ( ph -> ( Y H Z ) = ( Y ( Hom ` C ) Z ) )
14 9 13 eleqtrd 
 |-  ( ph -> G e. ( Y ( Hom ` C ) Z ) )
15 1 2 10 4 5 6 7 12 14 comfval 
 |-  ( ph -> ( G ( <. X , Y >. O Z ) F ) = ( G ( <. X , Y >. .x. Z ) F ) )