cofu2a

Description: Value of the morphism part of the functor composition. (Contributed by Zhi Wang, 16-Nov-2025)

	Ref	Expression
Hypotheses	cofu1a.b	$⊢ B = {Base}_{C}$
	cofu1a.f	$⊢ φ \to F (C Func D) G$
	cofu1a.k	$⊢ φ \to K (D Func E) L$
	cofu1a.m	$⊢ φ \to ⟨K, L⟩ \circ_{func} ⟨F, G⟩ = ⟨M, N⟩$
	cofu1a.x	$⊢ φ \to X \in B$
	cofu2a.y	$⊢ φ \to Y \in B$
	cofu2a.h	$⊢ H = Hom (C)$
	cofu2a.r	$⊢ φ \to R \in (X H Y)$
Assertion	cofu2a	$⊢ φ \to (F (X) L F (Y)) ((X G Y) (R)) = (X N Y) (R)$

Proof

Step	Hyp	Ref	Expression
1		cofu1a.b	$⊢ B = {Base}_{C}$
2		cofu1a.f	$⊢ φ \to F (C Func D) G$
3		cofu1a.k	$⊢ φ \to K (D Func E) L$
4		cofu1a.m	$⊢ φ \to ⟨K, L⟩ \circ_{func} ⟨F, G⟩ = ⟨M, N⟩$
5		cofu1a.x	$⊢ φ \to X \in B$
6		cofu2a.y	$⊢ φ \to Y \in B$
7		cofu2a.h	$⊢ H = Hom (C)$
8		cofu2a.r	$⊢ φ \to R \in (X H Y)$
9		df-br	$⊢ F (C Func D) G \leftrightarrow ⟨F, G⟩ \in (C Func D)$
10	2 9	sylib	$⊢ φ \to ⟨F, G⟩ \in (C Func D)$
11		df-br	$⊢ K (D Func E) L \leftrightarrow ⟨K, L⟩ \in (D Func E)$
12	3 11	sylib	$⊢ φ \to ⟨K, L⟩ \in (D Func E)$
13	1 10 12 5 6 7 8	cofu2	$⊢ φ \to (X 2^{nd} (⟨K, L⟩ \circ_{func} ⟨F, G⟩) Y) (R) = (1^{st} (⟨F, G⟩) (X) 2^{nd} (⟨K, L⟩) 1^{st} (⟨F, G⟩) (Y)) ((X 2^{nd} (⟨F, G⟩) Y) (R))$
14	4	fveq2d	$⊢ φ \to 2^{nd} (⟨K, L⟩ \circ_{func} ⟨F, G⟩) = 2^{nd} (⟨M, N⟩)$
15	10 12	cofucl	$⊢ φ \to ⟨K, L⟩ \circ_{func} ⟨F, G⟩ \in (C Func E)$
16	4 15	eqeltrrd	$⊢ φ \to ⟨M, N⟩ \in (C Func E)$
17		df-br	$⊢ M (C Func E) N \leftrightarrow ⟨M, N⟩ \in (C Func E)$
18	16 17	sylibr	$⊢ φ \to M (C Func E) N$
19	18	func2nd	$⊢ φ \to 2^{nd} (⟨M, N⟩) = N$
20	14 19	eqtrd	$⊢ φ \to 2^{nd} (⟨K, L⟩ \circ_{func} ⟨F, G⟩) = N$
21	20	oveqd	$⊢ φ \to X 2^{nd} (⟨K, L⟩ \circ_{func} ⟨F, G⟩) Y = X N Y$
22	21	fveq1d	$⊢ φ \to (X 2^{nd} (⟨K, L⟩ \circ_{func} ⟨F, G⟩) Y) (R) = (X N Y) (R)$
23	3	func2nd	$⊢ φ \to 2^{nd} (⟨K, L⟩) = L$
24	2	func1st	$⊢ φ \to 1^{st} (⟨F, G⟩) = F$
25	24	fveq1d	$⊢ φ \to 1^{st} (⟨F, G⟩) (X) = F (X)$
26	24	fveq1d	$⊢ φ \to 1^{st} (⟨F, G⟩) (Y) = F (Y)$
27	23 25 26	oveq123d	$⊢ φ \to 1^{st} (⟨F, G⟩) (X) 2^{nd} (⟨K, L⟩) 1^{st} (⟨F, G⟩) (Y) = F (X) L F (Y)$
28	2	func2nd	$⊢ φ \to 2^{nd} (⟨F, G⟩) = G$
29	28	oveqd	$⊢ φ \to X 2^{nd} (⟨F, G⟩) Y = X G Y$
30	29	fveq1d	$⊢ φ \to (X 2^{nd} (⟨F, G⟩) Y) (R) = (X G Y) (R)$
31	27 30	fveq12d	$⊢ φ \to (1^{st} (⟨F, G⟩) (X) 2^{nd} (⟨K, L⟩) 1^{st} (⟨F, G⟩) (Y)) ((X 2^{nd} (⟨F, G⟩) Y) (R)) = (F (X) L F (Y)) ((X G Y) (R))$
32	13 22 31	3eqtr3rd	$⊢ φ \to (F (X) L F (Y)) ((X G Y) (R)) = (X N Y) (R)$

Metamath Proof Explorer

Theorem cofu2a

Proof