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