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	5	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
10	9	funcrcl2	$$⊢\phi \to C\in \mathrm{Cat}$$
11		eqid	$$⊢D\mathrm{Nat}E=D\mathrm{Nat}E$$
12	11 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)$$
13	11 12	natrcl2	$$⊢\phi \to 1^{st}\left(G\right)\left(D\mathrm{Func}E\right)2^{nd}\left(G\right)$$
14	13	funcrcl2	$$⊢\phi \to D\in \mathrm{Cat}$$
15	13	funcrcl3	$$⊢\phi \to E\in \mathrm{Cat}$$
16		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 |-
17	10 14 15 16	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 |-
18		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 |-
19	17 18	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 |-
20	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 |-
21	19 20	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 |-
22		eqidd	$$⊢\phi \to ⟨G,F⟩=⟨G,F⟩$$
23		eqidd	$$⊢\phi \to ⟨H,F⟩=⟨H,F⟩$$
24		eqid	$$⊢C\mathrm{Nat}D=C\mathrm{Nat}D$$
25	3 24 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)$$
26	21 22 23 25 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)$$
27		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
28		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
29	9	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)$$
30	27 28 29	funcf1	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(F\right):{\mathrm{Base}}_C⟶{\mathrm{Base}}_D$$
31		simpr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to x\in {\mathrm{Base}}_C$$
32	30 31	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)$$
33	32	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)$$
34		eqid	$$⊢\mathrm{Id}\left(E\right)=\mathrm{Id}\left(E\right)$$
35	13	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)$$
36	30 31	ffvelcdmd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(F\right)\left(x\right)\in {\mathrm{Base}}_D$$
37	28 6 34 35 36	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)$$
38	33 37	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)$$
39	38	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)$$
40		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
41		eqid	$$⊢\mathrm{Hom}\left(E\right)=\mathrm{Hom}\left(E\right)$$
42	15	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to E\in \mathrm{Cat}$$
43	28 40 35	funcf1	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(G\right):{\mathrm{Base}}_D⟶{\mathrm{Base}}_E$$
44	43 36	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$$
45		eqid	$$⊢\mathrm{comp}\left(E\right)=\mathrm{comp}\left(E\right)$$
46	11 12	natrcl3	$$⊢\phi \to 1^{st}\left(H\right)\left(D\mathrm{Func}E\right)2^{nd}\left(H\right)$$
47	46	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)$$
48	28 40 47	funcf1	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(H\right):{\mathrm{Base}}_D⟶{\mathrm{Base}}_E$$
49	48 36	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$$
50	12	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)$$
51	11 50 28 41 36	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)$$
52	40 41 34 42 44 45 49 51	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)$$
53	39 52	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)$$
54	53	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)$$
55	8 26 54	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)$$