fucorid2

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. (Contributed by Zhi Wang, 11-Oct-2025)

	Ref	Expression
Hypotheses	fucolid.p	⊢ ( 𝜑 → ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) = 𝑃 )
	fucolid.i	⊢ 𝐼 = ( Id ‘ 𝑄 )
	fucorid.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	fucorid.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 ( 𝐷 Nat 𝐸 ) 𝐻 ) )
	fucorid.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
Assertion	fucorid2	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐺 , 𝐹 ⟩ 𝑃 ⟨ 𝐻 , 𝐹 ⟩ ) ( 𝐼 ‘ 𝐹 ) ) = ( 𝐴 ∘ ( 1^st ‘ 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucolid.p	⊢ ( 𝜑 → ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) = 𝑃 )
2		fucolid.i	⊢ 𝐼 = ( Id ‘ 𝑄 )
3		fucorid.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
4		fucorid.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 ( 𝐷 Nat 𝐸 ) 𝐻 ) )
5		fucorid.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
6	1 2 3 4 5	fucorid	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐺 , 𝐹 ⟩ 𝑃 ⟨ 𝐻 , 𝐹 ⟩ ) ( 𝐼 ‘ 𝐹 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝐴 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
7		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
8	7 4	nat1st2nd	⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ 𝐻 ) , ( 2^nd ‘ 𝐻 ) ⟩ ) )
9		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
10	7 8 9	natfn	⊢ ( 𝜑 → 𝐴 Fn ( Base ‘ 𝐷 ) )
11		dffn2	⊢ ( 𝐴 Fn ( Base ‘ 𝐷 ) ↔ 𝐴 : ( Base ‘ 𝐷 ) ⟶ V )
12	10 11	sylib	⊢ ( 𝜑 → 𝐴 : ( Base ‘ 𝐷 ) ⟶ V )
13		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
14		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
15		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
16	14 5 15	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
17	13 9 16	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
18		fcompt	⊢ ( ( 𝐴 : ( Base ‘ 𝐷 ) ⟶ V ∧ ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) ) → ( 𝐴 ∘ ( 1^st ‘ 𝐹 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝐴 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
19	12 17 18	syl2anc	⊢ ( 𝜑 → ( 𝐴 ∘ ( 1^st ‘ 𝐹 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝐴 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
20	6 19	eqtr4d	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐺 , 𝐹 ⟩ 𝑃 ⟨ 𝐻 , 𝐹 ⟩ ) ( 𝐼 ‘ 𝐹 ) ) = ( 𝐴 ∘ ( 1^st ‘ 𝐹 ) ) )

Metamath Proof Explorer

Theorem fucorid2

Proof