Theorem comfval2

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

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

Proof

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