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