Theorem mhpdeg

Description: All nonzero terms of a homogeneous polynomial have degree N . (Contributed by Steven Nguyen, 25-Aug-2023)

	Ref	Expression
Hypotheses	mhpdeg.h	$$⊢H=I\mathrm{mHomP}R$$
	mhpdeg.0	$$⊢\underset{\dot{}}{0}=0_R$$
	mhpdeg.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mhpdeg.i	$$⊢\phi \to I\in V$$
	mhpdeg.r	$$⊢\phi \to R\in W$$
	mhpdeg.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	mhpdeg.x	$$⊢\phi \to X\in H\left(N\right)$$
Assertion	mhpdeg	$$⊢\phi \to X\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}$$

Proof

Step	Hyp	Ref	Expression
1		mhpdeg.h	$$⊢H=I\mathrm{mHomP}R$$
2		mhpdeg.0	$$⊢\underset{\dot{}}{0}=0_R$$
3		mhpdeg.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
4		mhpdeg.i	$$⊢\phi \to I\in V$$
5		mhpdeg.r	$$⊢\phi \to R\in W$$
6		mhpdeg.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7		mhpdeg.x	$$⊢\phi \to X\in H\left(N\right)$$
8		eqid	$$⊢I\mathrm{mPoly}R=I\mathrm{mPoly}R$$
9		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
10	1 8 9 2 3 4 5 6	ismhp	$$⊢\phi \to \left(X\in H\left(N\right)\leftrightarrow \left(X\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}\wedge X\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\right)$$
11	10	simplbda	$$⊢\left(\phi \wedge X\in H\left(N\right)\right)\to X\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}$$
12	7 11	mpdan	$$⊢\phi \to X\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}$$