comfval2

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$
	comfval2.f	$⊢ φ \to F \in (X H Y)$
	comfval2.g	$⊢ φ \to G \in (Y H Z)$
Assertion	comfval2	$⊢ φ \to G (⟨X, Y⟩ O Z) F = 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		comfval2.f	$⊢ φ \to F \in (X H Y)$
9		comfval2.g	$⊢ φ \to G \in (Y H Z)$
10		eqid	$⊢ Hom (C) = Hom (C)$
11	3 2 10 5 6	homfval	$⊢ φ \to X H Y = X Hom (C) Y$
12	8 11	eleqtrd	$⊢ φ \to F \in (X Hom (C) Y)$
13	3 2 10 6 7	homfval	$⊢ φ \to Y H Z = Y Hom (C) Z$
14	9 13	eleqtrd	$⊢ φ \to G \in (Y Hom (C) Z)$
15	1 2 10 4 5 6 7 12 14	comfval	$⊢ φ \to G (⟨X, Y⟩ O Z) F = G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F$

Metamath Proof Explorer