comfval

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

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

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

Metamath Proof Explorer