Theorem comffval2

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$$
Assertion	comffval2	$$⊢\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)$$

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		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
9	1 2 8 4 5 6 7	comffval	$$⊢\phi \to ⟨X,Y⟩OZ=\left(g\in \left(Y\mathrm{Hom}\left(C\right)Z\right),f\in \left(X\mathrm{Hom}\left(C\right)Y\right)⟼g\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)f\right)$$
10	3 2 8 6 7	homfval	$$⊢\phi \to YHZ=Y\mathrm{Hom}\left(C\right)Z$$
11	3 2 8 5 6	homfval	$$⊢\phi \to XHY=X\mathrm{Hom}\left(C\right)Y$$
12		eqidd	$$⊢\phi \to g\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)f=g\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)f$$
13	10 11 12	mpoeq123dv	$$⊢\phi \to \left(g\in \left(YHZ\right),f\in \left(XHY\right)⟼g\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)f\right)=\left(g\in \left(Y\mathrm{Hom}\left(C\right)Z\right),f\in \left(X\mathrm{Hom}\left(C\right)Y\right)⟼g\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)f\right)$$
14	9 13	eqtr4d	$$⊢\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)$$