comffval

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$
Assertion	comffval	$⊢ φ \to ⟨X, Y⟩ O Z = (g \in (Y H Z), f \in (X H Y) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} Z) f)$

Proof

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	1 2 3 4	comfffval	$⊢ O = (x \in (B \times B), z \in B ⟼ (g \in (2^{nd} (x) H z), f \in H (x) ⟼ g (x \underset{˙}{\cdot} z) f))$
9	8	a1i	$⊢ φ \to O = (x \in (B \times B), z \in B ⟼ (g \in (2^{nd} (x) H z), f \in H (x) ⟼ g (x \underset{˙}{\cdot} z) f))$
10		simprl	$⊢ (φ \land (x = ⟨X, Y⟩ \land z = Z)) \to x = ⟨X, Y⟩$
11	10	fveq2d	$⊢ (φ \land (x = ⟨X, Y⟩ \land z = Z)) \to 2^{nd} (x) = 2^{nd} (⟨X, Y⟩)$
12		op2ndg	$⊢ (X \in B \land Y \in B) \to 2^{nd} (⟨X, Y⟩) = Y$
13	5 6 12	syl2anc	$⊢ φ \to 2^{nd} (⟨X, Y⟩) = Y$
14	13	adantr	$⊢ (φ \land (x = ⟨X, Y⟩ \land z = Z)) \to 2^{nd} (⟨X, Y⟩) = Y$
15	11 14	eqtrd	$⊢ (φ \land (x = ⟨X, Y⟩ \land z = Z)) \to 2^{nd} (x) = Y$
16		simprr	$⊢ (φ \land (x = ⟨X, Y⟩ \land z = Z)) \to z = Z$
17	15 16	oveq12d	$⊢ (φ \land (x = ⟨X, Y⟩ \land z = Z)) \to 2^{nd} (x) H z = Y H Z$
18	10	fveq2d	$⊢ (φ \land (x = ⟨X, Y⟩ \land z = Z)) \to H (x) = H (⟨X, Y⟩)$
19		df-ov	$⊢ X H Y = H (⟨X, Y⟩)$
20	18 19	eqtr4di	$⊢ (φ \land (x = ⟨X, Y⟩ \land z = Z)) \to H (x) = X H Y$
21	10 16	oveq12d	$⊢ (φ \land (x = ⟨X, Y⟩ \land z = Z)) \to x \underset{˙}{\cdot} z = ⟨X, Y⟩ \underset{˙}{\cdot} Z$
22	21	oveqd	$⊢ (φ \land (x = ⟨X, Y⟩ \land z = Z)) \to g (x \underset{˙}{\cdot} z) f = g (⟨X, Y⟩ \underset{˙}{\cdot} Z) f$
23	17 20 22	mpoeq123dv	$⊢ (φ \land (x = ⟨X, Y⟩ \land z = Z)) \to (g \in (2^{nd} (x) H z), f \in H (x) ⟼ g (x \underset{˙}{\cdot} z) f) = (g \in (Y H Z), f \in (X H Y) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} Z) f)$
24	5 6	opelxpd	$⊢ φ \to ⟨X, Y⟩ \in (B \times B)$
25		ovex	$⊢ Y H Z \in V$
26		ovex	$⊢ X H Y \in V$
27	25 26	mpoex	$⊢ (g \in (Y H Z), f \in (X H Y) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} Z) f) \in V$
28	27	a1i	$⊢ φ \to (g \in (Y H Z), f \in (X H Y) ⟼ g (⟨X, Y⟩ \underset{˙}{\cdot} Z) f) \in V$
29	9 23 24 7 28	ovmpod	$⊢ φ \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

Theorem comffval

Proof