comfffval2

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)$
Assertion	comfffval2	$⊢ O = (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) H y), f \in H (x) ⟼ g (x \underset{˙}{\cdot} y) f))$

Proof

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		eqid	$⊢ Hom (C) = Hom (C)$
6	1 2 5 4	comfffval	$⊢ O = (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) Hom (C) y), f \in Hom (C) (x) ⟼ g (x \underset{˙}{\cdot} y) f))$
7		xp2nd	$⊢ x \in (B \times B) \to 2^{nd} (x) \in B$
8	7	adantr	$⊢ (x \in (B \times B) \land y \in B) \to 2^{nd} (x) \in B$
9		simpr	$⊢ (x \in (B \times B) \land y \in B) \to y \in B$
10	3 2 5 8 9	homfval	$⊢ (x \in (B \times B) \land y \in B) \to 2^{nd} (x) H y = 2^{nd} (x) Hom (C) y$
11		xp1st	$⊢ x \in (B \times B) \to 1^{st} (x) \in B$
12	11	adantr	$⊢ (x \in (B \times B) \land y \in B) \to 1^{st} (x) \in B$
13	3 2 5 12 8	homfval	$⊢ (x \in (B \times B) \land y \in B) \to 1^{st} (x) H 2^{nd} (x) = 1^{st} (x) Hom (C) 2^{nd} (x)$
14		df-ov	$⊢ 1^{st} (x) H 2^{nd} (x) = H (⟨1^{st} (x), 2^{nd} (x)⟩)$
15		df-ov	$⊢ 1^{st} (x) Hom (C) 2^{nd} (x) = Hom (C) (⟨1^{st} (x), 2^{nd} (x)⟩)$
16	13 14 15	3eqtr3g	$⊢ (x \in (B \times B) \land y \in B) \to H (⟨1^{st} (x), 2^{nd} (x)⟩) = Hom (C) (⟨1^{st} (x), 2^{nd} (x)⟩)$
17		1st2nd2	$⊢ x \in (B \times B) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
18	17	adantr	$⊢ (x \in (B \times B) \land y \in B) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
19	18	fveq2d	$⊢ (x \in (B \times B) \land y \in B) \to H (x) = H (⟨1^{st} (x), 2^{nd} (x)⟩)$
20	18	fveq2d	$⊢ (x \in (B \times B) \land y \in B) \to Hom (C) (x) = Hom (C) (⟨1^{st} (x), 2^{nd} (x)⟩)$
21	16 19 20	3eqtr4d	$⊢ (x \in (B \times B) \land y \in B) \to H (x) = Hom (C) (x)$
22		eqidd	$⊢ (x \in (B \times B) \land y \in B) \to g (x \underset{˙}{\cdot} y) f = g (x \underset{˙}{\cdot} y) f$
23	10 21 22	mpoeq123dv	$⊢ (x \in (B \times B) \land y \in B) \to (g \in (2^{nd} (x) H y), f \in H (x) ⟼ g (x \underset{˙}{\cdot} y) f) = (g \in (2^{nd} (x) Hom (C) y), f \in Hom (C) (x) ⟼ g (x \underset{˙}{\cdot} y) f)$
24	23	mpoeq3ia	$⊢ (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) H y), f \in H (x) ⟼ g (x \underset{˙}{\cdot} y) f)) = (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) Hom (C) y), f \in Hom (C) (x) ⟼ g (x \underset{˙}{\cdot} y) f))$
25	6 24	eqtr4i	$⊢ O = (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) H y), f \in H (x) ⟼ g (x \underset{˙}{\cdot} y) f))$

Metamath Proof Explorer

Theorem comfffval2

Proof