Theorem fucolid

Description: Post-compose a natural transformation with an identity natural transformation. (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)$$
	fucolid.q	$$⊢Q=D\mathrm{FuncCat}E$$
	fucolid.a	$$⊢\phi \to A\in \left(G\left(C\mathrm{Nat}D\right)H\right)$$
	fucolid.f	$$⊢\phi \to F\in \left(D\mathrm{Func}E\right)$$
Assertion	fucolid	$$⊢\phi \to I\left(F\right)\left(⟨F,G⟩P⟨F,H⟩\right)A=\left(x\in {\mathrm{Base}}_C⟼\left(1^{st}\left(G\right)\left(x\right)2^{nd}\left(F\right)1^{st}\left(H\right)\left(x\right)\right)\left(A\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		fucolid.q	$$⊢Q=D\mathrm{FuncCat}E$$
4		fucolid.a	$$⊢\phi \to A\in \left(G\left(C\mathrm{Nat}D\right)H\right)$$
5		fucolid.f	$$⊢\phi \to F\in \left(D\mathrm{Func}E\right)$$
6		eqid	$$⊢\mathrm{Id}\left(E\right)=\mathrm{Id}\left(E\right)$$
7	3 2 6 5	fucid	$$⊢\phi \to I\left(F\right)=\mathrm{Id}\left(E\right)\circ 1^{st}\left(F\right)$$
8	7	oveq1d	$$⊢\phi \to I\left(F\right)\left(⟨F,G⟩P⟨F,H⟩\right)A=\left(\mathrm{Id}\left(E\right)\circ 1^{st}\left(F\right)\right)\left(⟨F,G⟩P⟨F,H⟩\right)A$$
9		eqid	$$⊢C\mathrm{Nat}D=C\mathrm{Nat}D$$
10	9 4	nat1st2nd	$$⊢\phi \to A\in \left(⟨1^{st}\left(G\right),2^{nd}\left(G\right)⟩\left(C\mathrm{Nat}D\right)⟨1^{st}\left(H\right),2^{nd}\left(H\right)⟩\right)$$
11	9 10	natrcl2	$$⊢\phi \to 1^{st}\left(G\right)\left(C\mathrm{Func}D\right)2^{nd}\left(G\right)$$
12	11	funcrcl2	$$⊢\phi \to C\in \mathrm{Cat}$$
13	11	funcrcl3	$$⊢\phi \to D\in \mathrm{Cat}$$
14	5	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(D\mathrm{Func}E\right)2^{nd}\left(F\right)$$
15	14	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	12 13 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 ⟨F,G⟩=⟨F,G⟩$$
23		eqidd	$$⊢\phi \to ⟨F,H⟩=⟨F,H⟩$$
24		eqid	$$⊢D\mathrm{Nat}E=D\mathrm{Nat}E$$
25	3 24 6 5	fucidcl	$$⊢\phi \to \mathrm{Id}\left(E\right)\circ 1^{st}\left(F\right)\in \left(F\left(D\mathrm{Nat}E\right)F\right)$$
26	21 22 23 4 25	fuco22a	$$⊢\phi \to \left(\mathrm{Id}\left(E\right)\circ 1^{st}\left(F\right)\right)\left(⟨F,G⟩P⟨F,H⟩\right)A=\left(x\in {\mathrm{Base}}_C⟼\left(\mathrm{Id}\left(E\right)\circ 1^{st}\left(F\right)\right)\left(1^{st}\left(H\right)\left(x\right)\right)\left(⟨1^{st}\left(F\right)\left(1^{st}\left(G\right)\left(x\right)\right),1^{st}\left(F\right)\left(1^{st}\left(H\right)\left(x\right)\right)⟩\mathrm{comp}\left(E\right)1^{st}\left(F\right)\left(1^{st}\left(H\right)\left(x\right)\right)\right)\left(1^{st}\left(G\right)\left(x\right)2^{nd}\left(F\right)1^{st}\left(H\right)\left(x\right)\right)\left(A\left(x\right)\right)\right)$$
27		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
28		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
29	14	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(F\right)\left(D\mathrm{Func}E\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}}_D⟶{\mathrm{Base}}_E$$
31		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
32	9 10	natrcl3	$$⊢\phi \to 1^{st}\left(H\right)\left(C\mathrm{Func}D\right)2^{nd}\left(H\right)$$
33	31 27 32	funcf1	$$⊢\phi \to 1^{st}\left(H\right):{\mathrm{Base}}_C⟶{\mathrm{Base}}_D$$
34	33	ffvelcdmda	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(H\right)\left(x\right)\in {\mathrm{Base}}_D$$
35	30 34	fvco3d	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to \left(\mathrm{Id}\left(E\right)\circ 1^{st}\left(F\right)\right)\left(1^{st}\left(H\right)\left(x\right)\right)=\mathrm{Id}\left(E\right)\left(1^{st}\left(F\right)\left(1^{st}\left(H\right)\left(x\right)\right)\right)$$
36	35	oveq1d	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to \left(\mathrm{Id}\left(E\right)\circ 1^{st}\left(F\right)\right)\left(1^{st}\left(H\right)\left(x\right)\right)\left(⟨1^{st}\left(F\right)\left(1^{st}\left(G\right)\left(x\right)\right),1^{st}\left(F\right)\left(1^{st}\left(H\right)\left(x\right)\right)⟩\mathrm{comp}\left(E\right)1^{st}\left(F\right)\left(1^{st}\left(H\right)\left(x\right)\right)\right)\left(1^{st}\left(G\right)\left(x\right)2^{nd}\left(F\right)1^{st}\left(H\right)\left(x\right)\right)\left(A\left(x\right)\right)=\mathrm{Id}\left(E\right)\left(1^{st}\left(F\right)\left(1^{st}\left(H\right)\left(x\right)\right)\right)\left(⟨1^{st}\left(F\right)\left(1^{st}\left(G\right)\left(x\right)\right),1^{st}\left(F\right)\left(1^{st}\left(H\right)\left(x\right)\right)⟩\mathrm{comp}\left(E\right)1^{st}\left(F\right)\left(1^{st}\left(H\right)\left(x\right)\right)\right)\left(1^{st}\left(G\right)\left(x\right)2^{nd}\left(F\right)1^{st}\left(H\right)\left(x\right)\right)\left(A\left(x\right)\right)$$
37		eqid	$$⊢\mathrm{Hom}\left(E\right)=\mathrm{Hom}\left(E\right)$$
38	15	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to E\in \mathrm{Cat}$$
39	31 27 11	funcf1	$$⊢\phi \to 1^{st}\left(G\right):{\mathrm{Base}}_C⟶{\mathrm{Base}}_D$$
40	39	ffvelcdmda	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(G\right)\left(x\right)\in {\mathrm{Base}}_D$$
41	30 40	ffvelcdmd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(F\right)\left(1^{st}\left(G\right)\left(x\right)\right)\in {\mathrm{Base}}_E$$
42		eqid	$$⊢\mathrm{comp}\left(E\right)=\mathrm{comp}\left(E\right)$$
43	30 34	ffvelcdmd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(F\right)\left(1^{st}\left(H\right)\left(x\right)\right)\in {\mathrm{Base}}_E$$
44		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
45	27 44 37 29 40 34	funcf2	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to \left(1^{st}\left(G\right)\left(x\right)2^{nd}\left(F\right)1^{st}\left(H\right)\left(x\right)\right):1^{st}\left(G\right)\left(x\right)\mathrm{Hom}\left(D\right)1^{st}\left(H\right)\left(x\right)⟶1^{st}\left(F\right)\left(1^{st}\left(G\right)\left(x\right)\right)\mathrm{Hom}\left(E\right)1^{st}\left(F\right)\left(1^{st}\left(H\right)\left(x\right)\right)$$
46	10	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(C\mathrm{Nat}D\right)⟨1^{st}\left(H\right),2^{nd}\left(H\right)⟩\right)$$
47		simpr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to x\in {\mathrm{Base}}_C$$
48	9 46 31 44 47	natcl	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to A\left(x\right)\in \left(1^{st}\left(G\right)\left(x\right)\mathrm{Hom}\left(D\right)1^{st}\left(H\right)\left(x\right)\right)$$
49	45 48	ffvelcdmd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to \left(1^{st}\left(G\right)\left(x\right)2^{nd}\left(F\right)1^{st}\left(H\right)\left(x\right)\right)\left(A\left(x\right)\right)\in \left(1^{st}\left(F\right)\left(1^{st}\left(G\right)\left(x\right)\right)\mathrm{Hom}\left(E\right)1^{st}\left(F\right)\left(1^{st}\left(H\right)\left(x\right)\right)\right)$$
50	28 37 6 38 41 42 43 49	catlid	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to \mathrm{Id}\left(E\right)\left(1^{st}\left(F\right)\left(1^{st}\left(H\right)\left(x\right)\right)\right)\left(⟨1^{st}\left(F\right)\left(1^{st}\left(G\right)\left(x\right)\right),1^{st}\left(F\right)\left(1^{st}\left(H\right)\left(x\right)\right)⟩\mathrm{comp}\left(E\right)1^{st}\left(F\right)\left(1^{st}\left(H\right)\left(x\right)\right)\right)\left(1^{st}\left(G\right)\left(x\right)2^{nd}\left(F\right)1^{st}\left(H\right)\left(x\right)\right)\left(A\left(x\right)\right)=\left(1^{st}\left(G\right)\left(x\right)2^{nd}\left(F\right)1^{st}\left(H\right)\left(x\right)\right)\left(A\left(x\right)\right)$$
51	36 50	eqtrd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to \left(\mathrm{Id}\left(E\right)\circ 1^{st}\left(F\right)\right)\left(1^{st}\left(H\right)\left(x\right)\right)\left(⟨1^{st}\left(F\right)\left(1^{st}\left(G\right)\left(x\right)\right),1^{st}\left(F\right)\left(1^{st}\left(H\right)\left(x\right)\right)⟩\mathrm{comp}\left(E\right)1^{st}\left(F\right)\left(1^{st}\left(H\right)\left(x\right)\right)\right)\left(1^{st}\left(G\right)\left(x\right)2^{nd}\left(F\right)1^{st}\left(H\right)\left(x\right)\right)\left(A\left(x\right)\right)=\left(1^{st}\left(G\right)\left(x\right)2^{nd}\left(F\right)1^{st}\left(H\right)\left(x\right)\right)\left(A\left(x\right)\right)$$
52	51	mpteq2dva	$$⊢\phi \to \left(x\in {\mathrm{Base}}_C⟼\left(\mathrm{Id}\left(E\right)\circ 1^{st}\left(F\right)\right)\left(1^{st}\left(H\right)\left(x\right)\right)\left(⟨1^{st}\left(F\right)\left(1^{st}\left(G\right)\left(x\right)\right),1^{st}\left(F\right)\left(1^{st}\left(H\right)\left(x\right)\right)⟩\mathrm{comp}\left(E\right)1^{st}\left(F\right)\left(1^{st}\left(H\right)\left(x\right)\right)\right)\left(1^{st}\left(G\right)\left(x\right)2^{nd}\left(F\right)1^{st}\left(H\right)\left(x\right)\right)\left(A\left(x\right)\right)\right)=\left(x\in {\mathrm{Base}}_C⟼\left(1^{st}\left(G\right)\left(x\right)2^{nd}\left(F\right)1^{st}\left(H\right)\left(x\right)\right)\left(A\left(x\right)\right)\right)$$
53	8 26 52	3eqtrd	$$⊢\phi \to I\left(F\right)\left(⟨F,G⟩P⟨F,H⟩\right)A=\left(x\in {\mathrm{Base}}_C⟼\left(1^{st}\left(G\right)\left(x\right)2^{nd}\left(F\right)1^{st}\left(H\right)\left(x\right)\right)\left(A\left(x\right)\right)\right)$$