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={\mathrm{Poly}}_1\left(R\right)$$
	mhmcoply1.q	$$⊢Q={\mathrm{Poly}}_1\left(S\right)$$
	mhmcoply1.b	$$⊢B={\mathrm{Base}}_P$$
	mhmcoply1.c	$$⊢C={\mathrm{Base}}_Q$$
	mhmcoply1.h	$$⊢\phi \to H\in \left(R\mathrm{MndHom}S\right)$$
	mhmcoply1.f	$$⊢\phi \to F\in B$$
Assertion	mhmcoply1	$$⊢\phi \to H\circ F\in C$$

Proof

Step	Hyp	Ref	Expression
1		mhmcoply1.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		mhmcoply1.q	$$⊢Q={\mathrm{Poly}}_1\left(S\right)$$
3		mhmcoply1.b	$$⊢B={\mathrm{Base}}_P$$
4		mhmcoply1.c	$$⊢C={\mathrm{Base}}_Q$$
5		mhmcoply1.h	$$⊢\phi \to H\in \left(R\mathrm{MndHom}S\right)$$
6		mhmcoply1.f	$$⊢\phi \to F\in B$$
7		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
8		eqid	$$⊢1_{𝑜}\mathrm{mPoly}S=1_{𝑜}\mathrm{mPoly}S$$
9	1 3	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
10	2 4	ply1bas	$$⊢C={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}S\right)}$$
11	7 8 9 10 5 6	mhmcompl	$$⊢\phi \to H\circ F\in C$$