Theorem mhpmpl

Description: A homogeneous polynomial is a polynomial. (Contributed by Steven Nguyen, 25-Aug-2023)

	Ref	Expression
Hypotheses	mhpmpl.h	$$⊢H=I\mathrm{mHomP}R$$
	mhpmpl.p	$$⊢P=I\mathrm{mPoly}R$$
	mhpmpl.b	$$⊢B={\mathrm{Base}}_P$$
	mhpmpl.i	$$⊢\phi \to I\in V$$
	mhpmpl.r	$$⊢\phi \to R\in W$$
	mhpmpl.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	mhpmpl.x	$$⊢\phi \to X\in H\left(N\right)$$
Assertion	mhpmpl	$$⊢\phi \to X\in B$$

Proof

Step	Hyp	Ref	Expression
1		mhpmpl.h	$$⊢H=I\mathrm{mHomP}R$$
2		mhpmpl.p	$$⊢P=I\mathrm{mPoly}R$$
3		mhpmpl.b	$$⊢B={\mathrm{Base}}_P$$
4		mhpmpl.i	$$⊢\phi \to I\in V$$
5		mhpmpl.r	$$⊢\phi \to R\in W$$
6		mhpmpl.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7		mhpmpl.x	$$⊢\phi \to X\in H\left(N\right)$$
8		eqid	$$⊢0_R=0_R$$
9		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\}$$
10	1 2 3 8 9 4 5 6	ismhp	$$⊢\phi \to \left(X\in H\left(N\right)\leftrightarrow \left(X\in B\wedge X\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	simprbda	$$⊢\left(\phi \wedge X\in H\left(N\right)\right)\to X\in B$$
12	7 11	mpdan	$$⊢\phi \to X\in B$$