cofid2

Description: Express the morphism part of ( G o.func F ) = I explicitly. (Contributed by Zhi Wang, 15-Nov-2025)

Step	Hyp	Ref	Expression
1		cofid1a.i	$⊢ I = {id}_{func} (D)$
2		cofid1a.b	$⊢ B = {Base}_{D}$
3		cofid1a.x	$⊢ φ \to X \in B$
4		cofid1.f	$⊢ φ \to F (D Func E) G$
5		cofid1.k	$⊢ φ \to K (E Func D) L$
6		cofid1.o	$⊢ φ \to ⟨K, L⟩ \circ_{func} ⟨F, G⟩ = I$
7		cofid2.y	$⊢ φ \to Y \in B$
8		cofid2.h	$⊢ H = Hom (D)$
9		cofid2.r	$⊢ φ \to R \in (X H Y)$
10	5	func2nd	$⊢ φ \to 2^{nd} (⟨K, L⟩) = L$
11	4	func1st	$⊢ φ \to 1^{st} (⟨F, G⟩) = F$
12	11	fveq1d	$⊢ φ \to 1^{st} (⟨F, G⟩) (X) = F (X)$
13	11	fveq1d	$⊢ φ \to 1^{st} (⟨F, G⟩) (Y) = F (Y)$
14	10 12 13	oveq123d	$⊢ φ \to 1^{st} (⟨F, G⟩) (X) 2^{nd} (⟨K, L⟩) 1^{st} (⟨F, G⟩) (Y) = F (X) L F (Y)$
15	4	func2nd	$⊢ φ \to 2^{nd} (⟨F, G⟩) = G$
16	15	oveqd	$⊢ φ \to X 2^{nd} (⟨F, G⟩) Y = X G Y$
17	16	fveq1d	$⊢ φ \to (X 2^{nd} (⟨F, G⟩) Y) (R) = (X G Y) (R)$
18	14 17	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))$
19		df-br	$⊢ F (D Func E) G \leftrightarrow ⟨F, G⟩ \in (D Func E)$
20	4 19	sylib	$⊢ φ \to ⟨F, G⟩ \in (D Func E)$
21		df-br	$⊢ K (E Func D) L \leftrightarrow ⟨K, L⟩ \in (E Func D)$
22	5 21	sylib	$⊢ φ \to ⟨K, L⟩ \in (E Func D)$
23	1 2 3 20 22 6 7 8 9	cofid2a	$⊢ φ \to (1^{st} (⟨F, G⟩) (X) 2^{nd} (⟨K, L⟩) 1^{st} (⟨F, G⟩) (Y)) ((X 2^{nd} (⟨F, G⟩) Y) (R)) = R$
24	18 23	eqtr3d	$⊢ φ \to (F (X) L F (Y)) ((X G Y) (R)) = R$

Metamath Proof Explorer