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	|- P = ( Poly1 ` R )
	mhmcoply1.q	|- Q = ( Poly1 ` S )
	mhmcoply1.b	|- B = ( Base ` P )
	mhmcoply1.c	|- C = ( Base ` Q )
	mhmcoply1.h	|- ( ph -> H e. ( R MndHom S ) )
	mhmcoply1.f	|- ( ph -> F e. B )
Assertion	mhmcoply1	|- ( ph -> ( H o. F ) e. C )

Proof

Step	Hyp	Ref	Expression
1		mhmcoply1.p	|- P = ( Poly1 ` R )
2		mhmcoply1.q	|- Q = ( Poly1 ` S )
3		mhmcoply1.b	|- B = ( Base ` P )
4		mhmcoply1.c	|- C = ( Base ` Q )
5		mhmcoply1.h	|- ( ph -> H e. ( R MndHom S ) )
6		mhmcoply1.f	|- ( ph -> F e. B )
7		eqid	|- ( 1o mPoly R ) = ( 1o mPoly R )
8		eqid	|- ( 1o mPoly S ) = ( 1o mPoly S )
9	1 3	ply1bas	|- B = ( Base ` ( 1o mPoly R ) )
10	2 4	ply1bas	|- C = ( Base ` ( 1o mPoly S ) )
11	7 8 9 10 5 6	mhmcompl	|- ( ph -> ( H o. F ) e. C )