Theorem cofid2a

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

	Ref	Expression
Hypotheses	cofid1a.i	$$⊢I={id}_{\mathrm{func}}\left(D\right)$$
	cofid1a.b	$$⊢B={\mathrm{Base}}_D$$
	cofid1a.x	$$⊢\phi \to X\in B$$
	cofid1a.f	$$⊢\phi \to F\in \left(D\mathrm{Func}E\right)$$
	cofid1a.g	$$⊢\phi \to G\in \left(E\mathrm{Func}D\right)$$
	cofid1a.o	$$⊢\phi \to G{\circ }_{\mathrm{func}}F=I$$
	cofid2a.y	$$⊢\phi \to Y\in B$$
	cofid2a.h	$$⊢H=\mathrm{Hom}\left(D\right)$$
	cofid2a.r	$$⊢\phi \to R\in \left(XHY\right)$$
Assertion	cofid2a	$$⊢\phi \to \left(1^{st}\left(F\right)\left(X\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(Y\right)\right)\left(\left(X{2}^{nd}\left(F\right)Y\right)\left(R\right)\right)=R$$

Proof

Step	Hyp	Ref	Expression
1		cofid1a.i	$$⊢I={id}_{\mathrm{func}}\left(D\right)$$
2		cofid1a.b	$$⊢B={\mathrm{Base}}_D$$
3		cofid1a.x	$$⊢\phi \to X\in B$$
4		cofid1a.f	$$⊢\phi \to F\in \left(D\mathrm{Func}E\right)$$
5		cofid1a.g	$$⊢\phi \to G\in \left(E\mathrm{Func}D\right)$$
6		cofid1a.o	$$⊢\phi \to G{\circ }_{\mathrm{func}}F=I$$
7		cofid2a.y	$$⊢\phi \to Y\in B$$
8		cofid2a.h	$$⊢H=\mathrm{Hom}\left(D\right)$$
9		cofid2a.r	$$⊢\phi \to R\in \left(XHY\right)$$
10	6	fveq2d	$$⊢\phi \to 2^{nd}\left(G{\circ }_{\mathrm{func}}F\right)=2^{nd}\left(I\right)$$
11	10	oveqd	$$⊢\phi \to X{2}^{nd}\left(G{\circ }_{\mathrm{func}}F\right)Y=X{2}^{nd}\left(I\right)Y$$
12	11	fveq1d	$$⊢\phi \to \left(X{2}^{nd}\left(G{\circ }_{\mathrm{func}}F\right)Y\right)\left(R\right)=\left(X{2}^{nd}\left(I\right)Y\right)\left(R\right)$$
13	2 4 5 3 7 8 9	cofu2	$$⊢\phi \to \left(X{2}^{nd}\left(G{\circ }_{\mathrm{func}}F\right)Y\right)\left(R\right)=\left(1^{st}\left(F\right)\left(X\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(Y\right)\right)\left(\left(X{2}^{nd}\left(F\right)Y\right)\left(R\right)\right)$$
14	4	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(D\mathrm{Func}E\right)2^{nd}\left(F\right)$$
15	14	funcrcl2	$$⊢\phi \to D\in \mathrm{Cat}$$
16	1 2 15 8 3 7 9	idfu2	$$⊢\phi \to \left(X{2}^{nd}\left(I\right)Y\right)\left(R\right)=R$$
17	12 13 16	3eqtr3d	$$⊢\phi \to \left(1^{st}\left(F\right)\left(X\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(Y\right)\right)\left(\left(X{2}^{nd}\left(F\right)Y\right)\left(R\right)\right)=R$$