Theorem comfval

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

	Ref	Expression
Hypotheses	comfffval.o	$$⊢O={\mathrm{comp}}_{𝑓}\left(C\right)$$
	comfffval.b	$$⊢B={\mathrm{Base}}_C$$
	comfffval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	comfffval.x	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
	comffval.x	$$⊢\phi \to X\in B$$
	comffval.y	$$⊢\phi \to Y\in B$$
	comffval.z	$$⊢\phi \to Z\in B$$
	comfval.f	$$⊢\phi \to F\in \left(XHY\right)$$
	comfval.g	$$⊢\phi \to G\in \left(YHZ\right)$$
Assertion	comfval	$$⊢\phi \to G\left(⟨X,Y⟩OZ\right)F=G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F$$

Proof

Step	Hyp	Ref	Expression
1		comfffval.o	$$⊢O={\mathrm{comp}}_{𝑓}\left(C\right)$$
2		comfffval.b	$$⊢B={\mathrm{Base}}_C$$
3		comfffval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
4		comfffval.x	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
5		comffval.x	$$⊢\phi \to X\in B$$
6		comffval.y	$$⊢\phi \to Y\in B$$
7		comffval.z	$$⊢\phi \to Z\in B$$
8		comfval.f	$$⊢\phi \to F\in \left(XHY\right)$$
9		comfval.g	$$⊢\phi \to G\in \left(YHZ\right)$$
10	1 2 3 4 5 6 7	comffval	$$⊢\phi \to ⟨X,Y⟩OZ=\left(g\in \left(YHZ\right),f\in \left(XHY\right)⟼g\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)f\right)$$
11		oveq12	$$⊢\left(g=G\wedge f=F\right)\to g\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)f=G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F$$
12	11	adantl	$$⊢\left(\phi \wedge \left(g=G\wedge f=F\right)\right)\to g\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)f=G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F$$
13		ovexd	$$⊢\phi \to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\in \mathrm{V}$$
14	10 12 9 8 13	ovmpod	$$⊢\phi \to G\left(⟨X,Y⟩OZ\right)F=G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F$$