Theorem mhmcoply1

Description: The composition of a monoid homomorphism and a polynomial is a polynomial. (Contributed by SN, 20-May-2025)

	Ref	Expression
Hypotheses	mhmcoply1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	mhmcoply1.q	⊢ 𝑄 = ( Poly1 ‘ 𝑆 )
	mhmcoply1.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	mhmcoply1.c	⊢ 𝐶 = ( Base ‘ 𝑄 )
	mhmcoply1.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
	mhmcoply1.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion	mhmcoply1	⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		mhmcoply1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		mhmcoply1.q	⊢ 𝑄 = ( Poly1 ‘ 𝑆 )
3		mhmcoply1.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		mhmcoply1.c	⊢ 𝐶 = ( Base ‘ 𝑄 )
5		mhmcoply1.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
6		mhmcoply1.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
8		eqid	⊢ ( 1o mPoly 𝑆 ) = ( 1o mPoly 𝑆 )
9	1 3	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
10	2 4	ply1bas	⊢ 𝐶 = ( Base ‘ ( 1o mPoly 𝑆 ) )
11	7 8 9 10 5 6	mhmcompl	⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ 𝐶 )