Theorem mhprcl

Description: Reverse closure for homogeneous polynomials, use elfvov1 and elfvov2 with reldmmhp for the reverse closure of I and R . (Contributed by SN, 4-Aug-2025)

	Ref	Expression
Hypotheses	mhprcl.h	$$⊢H=I\mathrm{mHomP}R$$
	mhprcl.x	$$⊢\phi \to X\in H\left(N\right)$$
Assertion	mhprcl	$$⊢\phi \to N\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		mhprcl.h	$$⊢H=I\mathrm{mHomP}R$$
2		mhprcl.x	$$⊢\phi \to X\in H\left(N\right)$$
3		eqid	$$⊢I\mathrm{mPoly}R=I\mathrm{mPoly}R$$
4		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
5		eqid	$$⊢0_R=0_R$$
6		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
7		reldmmhp	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mHomP}$$
8	7 1 2	elfvov1	$$⊢\phi \to I\in \mathrm{V}$$
9	7 1 2	elfvov2	$$⊢\phi \to R\in \mathrm{V}$$
10	1 3 4 5 6 8 9	mhpfval	$$⊢\phi \to H=\left(n\in {\mathbb{N}}_0⟼\left\{f\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}|f\mathrm{supp}{0}_R\subseteq \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=n\right\}\right\}\right)$$
11	10	fveq1d	$$⊢\phi \to H\left(N\right)=\left(n\in {\mathbb{N}}_0⟼\left\{f\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}|f\mathrm{supp}{0}_R\subseteq \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=n\right\}\right\}\right)\left(N\right)$$
12	2 11	eleqtrd	$$⊢\phi \to X\in \left(n\in {\mathbb{N}}_0⟼\left\{f\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}|f\mathrm{supp}{0}_R\subseteq \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=n\right\}\right\}\right)\left(N\right)$$
13		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼\left\{f\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}|f\mathrm{supp}{0}_R\subseteq \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=n\right\}\right\}\right)=\left(n\in {\mathbb{N}}_0⟼\left\{f\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}|f\mathrm{supp}{0}_R\subseteq \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=n\right\}\right\}\right)$$
14	13	mptrcl	$$⊢X\in \left(n\in {\mathbb{N}}_0⟼\left\{f\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}|f\mathrm{supp}{0}_R\subseteq \left\{g\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=n\right\}\right\}\right)\left(N\right)\to N\in {\mathbb{N}}_0$$
15	12 14	syl	$$⊢\phi \to N\in {\mathbb{N}}_0$$