Theorem fucorid

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, in maps-to notation. (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	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)$$

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		eqid	$$⊢\mathrm{Id}\left(D\right)=\mathrm{Id}\left(D\right)$$
7	3 2 6 5	fucid	$$⊢\phi \to I\left(F\right)=\mathrm{Id}\left(D\right)\circ 1^{st}\left(F\right)$$
8	7	oveq2d	$$⊢\phi \to A\left(⟨G,F⟩P⟨H,F⟩\right)I\left(F\right)=A\left(⟨G,F⟩P⟨H,F⟩\right)\left(\mathrm{Id}\left(D\right)\circ 1^{st}\left(F\right)\right)$$
9		eqid	$$⊢C\mathrm{Nat}D=C\mathrm{Nat}D$$
10	3 9 6 5	fucidcl	$$⊢\phi \to \mathrm{Id}\left(D\right)\circ 1^{st}\left(F\right)\in \left(F\left(C\mathrm{Nat}D\right)F\right)$$
11	9 10	nat1st2nd	$$⊢\phi \to \mathrm{Id}\left(D\right)\circ 1^{st}\left(F\right)\in \left(⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩\left(C\mathrm{Nat}D\right)⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩\right)$$
12	9 11	natrcl2	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
13	12	funcrcl2	$$⊢\phi \to C\in \mathrm{Cat}$$
14		eqid	$$⊢D\mathrm{Nat}E=D\mathrm{Nat}E$$
15	14 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)$$
16	14 15	natrcl2	$$⊢\phi \to 1^{st}\left(G\right)\left(D\mathrm{Func}E\right)2^{nd}\left(G\right)$$
17	16	funcrcl2	$$⊢\phi \to D\in \mathrm{Cat}$$
18	16	funcrcl3	$$⊢\phi \to E\in \mathrm{Cat}$$
19		eqidd	Could not format ( ph -> ( <. C , D >. o.F E ) = ( <. C , D >. o.F E ) ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = ( <. C , D >. o.F E ) ) with typecode |-
20	13 17 18 19	fucoelvv	Could not format ( ph -> ( <. C , D >. o.F E ) e. ( _V X. _V ) ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) e. ( _V X. _V ) ) with typecode |-
21		1st2nd2	Could not format ( ( <. C , D >. o.F E ) e. ( _V X. _V ) -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) : No typesetting found for |- ( ( <. C , D >. o.F E ) e. ( _V X. _V ) -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) with typecode |-
22	20 21	syl	Could not format ( ph -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) with typecode |-
23	1	opeq2d	Could not format ( ph -> <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. = <. ( 1st ` ( <. C , D >. o.F E ) ) , P >. ) : No typesetting found for |- ( ph -> <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. = <. ( 1st ` ( <. C , D >. o.F E ) ) , P >. ) with typecode |-
24	22 23	eqtrd	Could not format ( ph -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , P >. ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , P >. ) with typecode |-
25		eqidd	$$⊢\phi \to ⟨G,F⟩=⟨G,F⟩$$
26		eqidd	$$⊢\phi \to ⟨H,F⟩=⟨H,F⟩$$
27	24 25 26 10 4	fuco22a	$$⊢\phi \to A\left(⟨G,F⟩P⟨H,F⟩\right)\left(\mathrm{Id}\left(D\right)\circ 1^{st}\left(F\right)\right)=\left(x\in {\mathrm{Base}}_C⟼A\left(1^{st}\left(F\right)\left(x\right)\right)\left(⟨1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(x\right)\right),1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(x\right)\right)⟩\mathrm{comp}\left(E\right)1^{st}\left(H\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(x\right)\right)\left(\left(\mathrm{Id}\left(D\right)\circ 1^{st}\left(F\right)\right)\left(x\right)\right)\right)$$
28		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
29		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
30	12	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
31	28 29 30	funcf1	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(F\right):{\mathrm{Base}}_C⟶{\mathrm{Base}}_D$$
32		simpr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to x\in {\mathrm{Base}}_C$$
33	31 32	fvco3d	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to \left(\mathrm{Id}\left(D\right)\circ 1^{st}\left(F\right)\right)\left(x\right)=\mathrm{Id}\left(D\right)\left(1^{st}\left(F\right)\left(x\right)\right)$$
34	33	fveq2d	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to \left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(x\right)\right)\left(\left(\mathrm{Id}\left(D\right)\circ 1^{st}\left(F\right)\right)\left(x\right)\right)=\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(x\right)\right)\left(\mathrm{Id}\left(D\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)$$
35		eqid	$$⊢\mathrm{Id}\left(E\right)=\mathrm{Id}\left(E\right)$$
36	16	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(G\right)\left(D\mathrm{Func}E\right)2^{nd}\left(G\right)$$
37	31 32	ffvelcdmd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(F\right)\left(x\right)\in {\mathrm{Base}}_D$$
38	29 6 35 36 37	funcid	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to \left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(x\right)\right)\left(\mathrm{Id}\left(D\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)=\mathrm{Id}\left(E\right)\left(1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)$$
39	34 38	eqtrd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to \left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(x\right)\right)\left(\left(\mathrm{Id}\left(D\right)\circ 1^{st}\left(F\right)\right)\left(x\right)\right)=\mathrm{Id}\left(E\right)\left(1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)$$
40	39	oveq2d	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to A\left(1^{st}\left(F\right)\left(x\right)\right)\left(⟨1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(x\right)\right),1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(x\right)\right)⟩\mathrm{comp}\left(E\right)1^{st}\left(H\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(x\right)\right)\left(\left(\mathrm{Id}\left(D\right)\circ 1^{st}\left(F\right)\right)\left(x\right)\right)=A\left(1^{st}\left(F\right)\left(x\right)\right)\left(⟨1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(x\right)\right),1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(x\right)\right)⟩\mathrm{comp}\left(E\right)1^{st}\left(H\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)\mathrm{Id}\left(E\right)\left(1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)$$
41		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
42		eqid	$$⊢\mathrm{Hom}\left(E\right)=\mathrm{Hom}\left(E\right)$$
43	18	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to E\in \mathrm{Cat}$$
44	29 41 36	funcf1	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(G\right):{\mathrm{Base}}_D⟶{\mathrm{Base}}_E$$
45	44 37	ffvelcdmd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(x\right)\right)\in {\mathrm{Base}}_E$$
46		eqid	$$⊢\mathrm{comp}\left(E\right)=\mathrm{comp}\left(E\right)$$
47	14 15	natrcl3	$$⊢\phi \to 1^{st}\left(H\right)\left(D\mathrm{Func}E\right)2^{nd}\left(H\right)$$
48	47	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(H\right)\left(D\mathrm{Func}E\right)2^{nd}\left(H\right)$$
49	29 41 48	funcf1	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(H\right):{\mathrm{Base}}_D⟶{\mathrm{Base}}_E$$
50	49 37	ffvelcdmd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(H\right)\left(1^{st}\left(F\right)\left(x\right)\right)\in {\mathrm{Base}}_E$$
51	15	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\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)$$
52	14 51 29 42 37	natcl	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to A\left(1^{st}\left(F\right)\left(x\right)\right)\in \left(1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(x\right)\right)\mathrm{Hom}\left(E\right)1^{st}\left(H\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)$$
53	41 42 35 43 45 46 50 52	catrid	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to A\left(1^{st}\left(F\right)\left(x\right)\right)\left(⟨1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(x\right)\right),1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(x\right)\right)⟩\mathrm{comp}\left(E\right)1^{st}\left(H\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)\mathrm{Id}\left(E\right)\left(1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)=A\left(1^{st}\left(F\right)\left(x\right)\right)$$
54	40 53	eqtrd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to A\left(1^{st}\left(F\right)\left(x\right)\right)\left(⟨1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(x\right)\right),1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(x\right)\right)⟩\mathrm{comp}\left(E\right)1^{st}\left(H\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(x\right)\right)\left(\left(\mathrm{Id}\left(D\right)\circ 1^{st}\left(F\right)\right)\left(x\right)\right)=A\left(1^{st}\left(F\right)\left(x\right)\right)$$
55	54	mpteq2dva	$$⊢\phi \to \left(x\in {\mathrm{Base}}_C⟼A\left(1^{st}\left(F\right)\left(x\right)\right)\left(⟨1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(x\right)\right),1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(x\right)\right)⟩\mathrm{comp}\left(E\right)1^{st}\left(H\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(x\right)\right)\left(\left(\mathrm{Id}\left(D\right)\circ 1^{st}\left(F\right)\right)\left(x\right)\right)\right)=\left(x\in {\mathrm{Base}}_C⟼A\left(1^{st}\left(F\right)\left(x\right)\right)\right)$$
56	8 27 55	3eqtrd	$$⊢\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)$$