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.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.h	$$⊢\phi \to H\in \left(R\mathrm{MndHom}S\right)$$
6		mhmcompl.f	$$⊢\phi \to F\in B$$
7		fvexd	$$⊢\phi \to {\mathrm{Base}}_S\in \mathrm{V}$$
8		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\}$$
9		ovexd	$$⊢\phi \to {{\mathbb{N}}_0}^I\in \mathrm{V}$$
10	8 9	rabexd	$$⊢\phi \to \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
11		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
12		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
13	11 12	mhmf	$$⊢H\in \left(R\mathrm{MndHom}S\right)\to H:{\mathrm{Base}}_R⟶{\mathrm{Base}}_S$$
14	5 13	syl	$$⊢\phi \to H:{\mathrm{Base}}_R⟶{\mathrm{Base}}_S$$
15	1 11 3 8 6	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$$
16	14 15	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$$
17	7 10 16	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)$$
18		eqid	$$⊢I\mathrm{mPwSer}S=I\mathrm{mPwSer}S$$
19		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}$$
20	1 3	mplrcl	$$⊢F\in B\to I\in \mathrm{V}$$
21	6 20	syl	$$⊢\phi \to I\in \mathrm{V}$$
22	18 12 8 19 21	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	17 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	5 25	syl	$$⊢\phi \to R\in \mathrm{Mnd}$$
27		eqid	$$⊢0_R=0_R$$
28	11 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 6 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	5 34	syl	$$⊢\phi \to H\left(0_R\right)=0_S$$
36	24 29 15 14 30 10 31 32 35	fsuppcor	$$⊢\phi \to {finSupp}_{0_S}\left(\left(H\circ F\right)\right)$$
37	2 18 19 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$$