Theorem mhmcompl

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

	Ref	Expression
Hypotheses	mhmcompl.p	$$⊢P=I\mathrm{mPoly}R$$
	mhmcompl.q	$$⊢Q=I\mathrm{mPoly}S$$
	mhmcompl.b	$$⊢B={\mathrm{Base}}_P$$
	mhmcompl.c	$$⊢C={\mathrm{Base}}_Q$$
	mhmcompl.i	$$⊢\phi \to I\in V$$
	mhmcompl.h	$$⊢\phi \to H\in \left(R\mathrm{MndHom}S\right)$$
	mhmcompl.f	$$⊢\phi \to F\in B$$
Assertion	mhmcompl	$$⊢\phi \to H\circ F\in C$$

Proof

Step	Hyp	Ref	Expression
1		mhmcompl.p	$$⊢P=I\mathrm{mPoly}R$$
2		mhmcompl.q	$$⊢Q=I\mathrm{mPoly}S$$
3		mhmcompl.b	$$⊢B={\mathrm{Base}}_P$$
4		mhmcompl.c	$$⊢C={\mathrm{Base}}_Q$$
5		mhmcompl.i	$$⊢\phi \to I\in V$$
6		mhmcompl.h	$$⊢\phi \to H\in \left(R\mathrm{MndHom}S\right)$$
7		mhmcompl.f	$$⊢\phi \to F\in B$$
8		fvexd	$$⊢\phi \to {\mathrm{Base}}_S\in \mathrm{V}$$
9		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
10	9	rabex	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
11	10	a1i	$$⊢\phi \to \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
12		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
13		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
14	12 13	mhmf	$$⊢H\in \left(R\mathrm{MndHom}S\right)\to H:{\mathrm{Base}}_R⟶{\mathrm{Base}}_S$$
15	6 14	syl	$$⊢\phi \to H:{\mathrm{Base}}_R⟶{\mathrm{Base}}_S$$
16		eqid	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
17	1 12 3 16 7	mplelf	$$⊢\phi \to F:\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
18	15 17	fcod	$$⊢\phi \to \left(H\circ F\right):\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_S$$
19	8 11 18	elmapdd	$$⊢\phi \to H\circ F\in \left({{\mathrm{Base}}_S}^{\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}\right)$$
20		eqid	$$⊢I\mathrm{mPwSer}S=I\mathrm{mPwSer}S$$
21		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}$$
22	20 13 16 21 5	psrbas	$$⊢\phi \to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}={{\mathrm{Base}}_S}^{\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}$$
23	19 22	eleqtrrd	$$⊢\phi \to H\circ F\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}$$
24		fvexd	$$⊢\phi \to 0_S\in \mathrm{V}$$
25		mhmrcl1	$$⊢H\in \left(R\mathrm{MndHom}S\right)\to R\in \mathrm{Mnd}$$
26	6 25	syl	$$⊢\phi \to R\in \mathrm{Mnd}$$
27		eqid	$$⊢0_R=0_R$$
28	12 27	mndidcl	$$⊢R\in \mathrm{Mnd}\to 0_R\in {\mathrm{Base}}_R$$
29	26 28	syl	$$⊢\phi \to 0_R\in {\mathrm{Base}}_R$$
30		ssidd	$$⊢\phi \to {\mathrm{Base}}_R\subseteq {\mathrm{Base}}_R$$
31		fvexd	$$⊢\phi \to {\mathrm{Base}}_R\in \mathrm{V}$$
32	1 3 27 7 26	mplelsfi	$$⊢\phi \to {finSupp}_{0_R}\left(F\right)$$
33		eqid	$$⊢0_S=0_S$$
34	27 33	mhm0	$$⊢H\in \left(R\mathrm{MndHom}S\right)\to H\left(0_R\right)=0_S$$
35	6 34	syl	$$⊢\phi \to H\left(0_R\right)=0_S$$
36	24 29 17 15 30 11 31 32 35	fsuppcor	$$⊢\phi \to {finSupp}_{0_S}\left(\left(H\circ F\right)\right)$$
37	2 20 21 33 4	mplelbas	$$⊢H\circ F\in C\leftrightarrow \left(H\circ F\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}\wedge {finSupp}_{0_S}\left(\left(H\circ F\right)\right)\right)$$
38	23 36 37	sylanbrc	$$⊢\phi \to H\circ F\in C$$