Theorem fucoridid

Description: Horizontal composition with the identity natural transformation of the identity functor leaves a natural transformation unchanged. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

	Ref	Expression
Hypotheses	fucoridid.p	⊢ ( 𝜑 → ( 2nd ‘ ( ⟨ 𝐶 , 𝐶 ⟩ ∘F 𝐸 ) ) = 𝑃 )
	fucoridid.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐶 )
	fucoridid.j	⊢ 𝐽 = ( Id ‘ 𝑄 )
	fucoridid.i	⊢ 𝐼 = ( idfunc ‘ 𝐶 )
	fucoridid.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	fucoridid.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 ( 𝐶 Nat 𝐸 ) 𝐻 ) )
Assertion	fucoridid	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐺 , 𝐼 ⟩ 𝑃 ⟨ 𝐻 , 𝐼 ⟩ ) ( 𝐽 ‘ 𝐼 ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fucoridid.p	⊢ ( 𝜑 → ( 2nd ‘ ( ⟨ 𝐶 , 𝐶 ⟩ ∘F 𝐸 ) ) = 𝑃 )
2		fucoridid.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐶 )
3		fucoridid.j	⊢ 𝐽 = ( Id ‘ 𝑄 )
4		fucoridid.i	⊢ 𝐼 = ( idfunc ‘ 𝐶 )
5		fucoridid.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
6		fucoridid.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 ( 𝐶 Nat 𝐸 ) 𝐻 ) )
7	4	idfucl	⊢ ( 𝐶 ∈ Cat → 𝐼 ∈ ( 𝐶 Func 𝐶 ) )
8	5 7	syl	⊢ ( 𝜑 → 𝐼 ∈ ( 𝐶 Func 𝐶 ) )
9	1 3 2 6 8	fucorid2	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐺 , 𝐼 ⟩ 𝑃 ⟨ 𝐻 , 𝐼 ⟩ ) ( 𝐽 ‘ 𝐼 ) ) = ( 𝐴 ∘ ( 1st ‘ 𝐼 ) ) )
10		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
11	4 10 5	idfu1st	⊢ ( 𝜑 → ( 1st ‘ 𝐼 ) = ( I ↾ ( Base ‘ 𝐶 ) ) )
12	11	coeq2d	⊢ ( 𝜑 → ( 𝐴 ∘ ( 1st ‘ 𝐼 ) ) = ( 𝐴 ∘ ( I ↾ ( Base ‘ 𝐶 ) ) ) )
13		eqid	⊢ ( 𝐶 Nat 𝐸 ) = ( 𝐶 Nat 𝐸 )
14	13 10 6	natfn2	⊢ ( 𝜑 → 𝐴 Fn ( Base ‘ 𝐶 ) )
15		dffn2	⊢ ( 𝐴 Fn ( Base ‘ 𝐶 ) ↔ 𝐴 : ( Base ‘ 𝐶 ) ⟶ V )
16	14 15	sylib	⊢ ( 𝜑 → 𝐴 : ( Base ‘ 𝐶 ) ⟶ V )
17		fcoi1	⊢ ( 𝐴 : ( Base ‘ 𝐶 ) ⟶ V → ( 𝐴 ∘ ( I ↾ ( Base ‘ 𝐶 ) ) ) = 𝐴 )
18	16 17	syl	⊢ ( 𝜑 → ( 𝐴 ∘ ( I ↾ ( Base ‘ 𝐶 ) ) ) = 𝐴 )
19	9 12 18	3eqtrd	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐺 , 𝐼 ⟩ 𝑃 ⟨ 𝐻 , 𝐼 ⟩ ) ( 𝐽 ‘ 𝐼 ) ) = 𝐴 )