Theorem fucorid2

Description: Pre-composing a natural transformation with the identity natural transformation of a functor is pre-composing it with the object part of the functor. (Contributed by Zhi Wang, 11-Oct-2025)

	Ref	Expression
Hypotheses	fucolid.p	No typesetting found for |- ( ph -> ( 2nd ` ( <. C , D >. o.F E ) ) = P ) with typecode |-
	fucolid.i	$$⊢I=\mathrm{Id}\left(Q\right)$$
	fucorid.q	$$⊢Q=C\mathrm{FuncCat}D$$
	fucorid.a	$$⊢\phi \to A\in \left(G\left(D\mathrm{Nat}E\right)H\right)$$
	fucorid.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
Assertion	fucorid2	$$⊢\phi \to A\left(⟨G,F⟩P⟨H,F⟩\right)I\left(F\right)=A\circ 1^{st}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		fucolid.p	Could not format ( ph -> ( 2nd ` ( <. C , D >. o.F E ) ) = P ) : No typesetting found for |- ( ph -> ( 2nd ` ( <. C , D >. o.F E ) ) = P ) with typecode |-
2		fucolid.i	$$⊢I=\mathrm{Id}\left(Q\right)$$
3		fucorid.q	$$⊢Q=C\mathrm{FuncCat}D$$
4		fucorid.a	$$⊢\phi \to A\in \left(G\left(D\mathrm{Nat}E\right)H\right)$$
5		fucorid.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
6	1 2 3 4 5	fucorid	$$⊢\phi \to A\left(⟨G,F⟩P⟨H,F⟩\right)I\left(F\right)=\left(x\in {\mathrm{Base}}_C⟼A\left(1^{st}\left(F\right)\left(x\right)\right)\right)$$
7		eqid	$$⊢D\mathrm{Nat}E=D\mathrm{Nat}E$$
8	7 4	nat1st2nd	$$⊢\phi \to A\in \left(⟨1^{st}\left(G\right),2^{nd}\left(G\right)⟩\left(D\mathrm{Nat}E\right)⟨1^{st}\left(H\right),2^{nd}\left(H\right)⟩\right)$$
9		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
10	7 8 9	natfn	$$⊢\phi \to AFn{\mathrm{Base}}_D$$
11		dffn2	$$⊢AFn{\mathrm{Base}}_D\leftrightarrow A:{\mathrm{Base}}_D⟶\mathrm{V}$$
12	10 11	sylib	$$⊢\phi \to A:{\mathrm{Base}}_D⟶\mathrm{V}$$
13		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
14	5	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
15	13 9 14	funcf1	$$⊢\phi \to 1^{st}\left(F\right):{\mathrm{Base}}_C⟶{\mathrm{Base}}_D$$
16		fcompt	$$⊢\left(A:{\mathrm{Base}}_D⟶\mathrm{V}\wedge 1^{st}\left(F\right):{\mathrm{Base}}_C⟶{\mathrm{Base}}_D\right)\to A\circ 1^{st}\left(F\right)=\left(x\in {\mathrm{Base}}_C⟼A\left(1^{st}\left(F\right)\left(x\right)\right)\right)$$
17	12 15 16	syl2anc	$$⊢\phi \to A\circ 1^{st}\left(F\right)=\left(x\in {\mathrm{Base}}_C⟼A\left(1^{st}\left(F\right)\left(x\right)\right)\right)$$
18	6 17	eqtr4d	$$⊢\phi \to A\left(⟨G,F⟩P⟨H,F⟩\right)I\left(F\right)=A\circ 1^{st}\left(F\right)$$