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