Theorem fucoaltval

Description: At a pair consisting of a natural transformation and the identity of the identity functor, post-composed functor composition acts by the post- composing functor on that natural transformation. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

	Ref	Expression
Hypotheses	fucoaltfunc.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
	fucoaltval.l	⊢ 𝐿 = ( ⟨ 𝐶 , 𝐶 ⟩ ∘F 𝐸 )
	fucoaltval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	fucoaltval.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
	fucoaltval.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑄 Func 𝑄 ) )
	fucoaltval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐸 ) )
	fucoaltval.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
	fucoaltval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) )
	fucoaltval.i	⊢ 𝐼 = ( idfunc ‘ 𝐶 )
	fucoaltval.j	⊢ 𝐽 = ( Id ‘ ( 𝐶 FuncCat 𝐶 ) )
Assertion	fucoaltval	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐹 , 𝐼 ⟩ ( 2nd ‘ ( 𝐾 ∘func 𝐿 ) ) ⟨ 𝐺 , 𝐼 ⟩ ) ( 𝐽 ‘ 𝐼 ) ) = ( ( 𝐹 ( 2nd ‘ 𝐾 ) 𝐺 ) ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		fucoaltfunc.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
2		fucoaltval.l	⊢ 𝐿 = ( ⟨ 𝐶 , 𝐶 ⟩ ∘F 𝐸 )
3		fucoaltval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		fucoaltval.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
5		fucoaltval.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑄 Func 𝑄 ) )
6		fucoaltval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐸 ) )
7		fucoaltval.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
8		fucoaltval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) )
9		fucoaltval.i	⊢ 𝐼 = ( idfunc ‘ 𝐶 )
10		fucoaltval.j	⊢ 𝐽 = ( Id ‘ ( 𝐶 FuncCat 𝐶 ) )
11		eqid	⊢ ( ( 𝐶 FuncCat 𝐸 ) ×c ( 𝐶 FuncCat 𝐶 ) ) = ( ( 𝐶 FuncCat 𝐸 ) ×c ( 𝐶 FuncCat 𝐶 ) )
12	1 2 3 4 5 6 7 8 9 10 11	fucoaltvallem	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐹 , 𝐼 ⟩ ( 2nd ‘ ( 𝐾 ∘func 𝐿 ) ) ⟨ 𝐺 , 𝐼 ⟩ ) ( 𝐽 ‘ 𝐼 ) ) = ( ( 𝐹 ( 2nd ‘ 𝐾 ) 𝐺 ) ‘ 𝐴 ) )