comffval2

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

	Ref	Expression
Hypotheses	comfffval2.o	$⊢ O = {comp}_{𝑓} (C)$
	comfffval2.b	$⊢ B = {Base}_{C}$
	comfffval2.h	$⊢ H = {Hom}_{𝑓} (C)$
	comfffval2.x	$⊢ \underset{˙}{\cdot} = comp (C)$
	comffval2.x	$⊢ φ \to X \in B$
	comffval2.y	$⊢ φ \to Y \in B$
	comffval2.z	$⊢ φ \to Z \in B$
Assertion	comffval2	$⊢ φ \to ⟨X, Y⟩ O Z = (g \in (Y H Z), f \in (X H Y) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} Z) f)$

Step	Hyp	Ref	Expression
1		comfffval2.o	$⊢ O = {comp}_{𝑓} (C)$
2		comfffval2.b	$⊢ B = {Base}_{C}$
3		comfffval2.h	$⊢ H = {Hom}_{𝑓} (C)$
4		comfffval2.x	$⊢ \underset{˙}{\cdot} = comp (C)$
5		comffval2.x	$⊢ φ \to X \in B$
6		comffval2.y	$⊢ φ \to Y \in B$
7		comffval2.z	$⊢ φ \to Z \in B$
8		eqid	$⊢ Hom (C) = Hom (C)$
9	1 2 8 4 5 6 7	comffval	$⊢ φ \to ⟨X, Y⟩ O Z = (g \in (Y Hom (C) Z), f \in (X Hom (C) Y) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} Z) f)$
10	3 2 8 6 7	homfval	$⊢ φ \to Y H Z = Y Hom (C) Z$
11	3 2 8 5 6	homfval	$⊢ φ \to X H Y = X Hom (C) Y$
12		eqidd	$⊢ φ \to g (⟨X, Y⟩ \underset{˙}{\cdot} Z) f = g (⟨X, Y⟩ \underset{˙}{\cdot} Z) f$
13	10 11 12	mpoeq123dv	$⊢ φ \to (g \in (Y H Z), f \in (X H Y) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} Z) f) = (g \in (Y Hom (C) Z), f \in (X Hom (C) Y) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} Z) f)$
14	9 13	eqtr4d	$⊢ φ \to ⟨X, Y⟩ O Z = (g \in (Y H Z), f \in (X H Y) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} Z) f)$

Metamath Proof Explorer