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 mHomP R$
	mhpdeg.0	$⊢ \underset{˙}{0} = 0_{R}$
	mhpdeg.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
	mhpdeg.x	$⊢ φ \to X \in H (N)$
Assertion	mhpdeg	$⊢ φ \to X supp \underset{˙}{0} \subseteq \{g \in D \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}$

Step	Hyp	Ref	Expression
1		mhpdeg.h	$⊢ H = I mHomP R$
2		mhpdeg.0	$⊢ \underset{˙}{0} = 0_{R}$
3		mhpdeg.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
4		mhpdeg.x	$⊢ φ \to X \in H (N)$
5		eqid	$⊢ I mPoly R = I mPoly R$
6		eqid	$⊢ {Base}_{(I mPoly R)} = {Base}_{(I mPoly R)}$
7	1 4	mhprcl	$⊢ φ \to N \in ℕ_{0}$
8	1 5 6 2 3 7	ismhp	$⊢ φ \to (X \in H (N) \leftrightarrow (X \in {Base}_{(I mPoly R)} \land X supp \underset{˙}{0} \subseteq \{g \in D \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}))$
9	8	simplbda	$⊢ (φ \land X \in H (N)) \to X supp \underset{˙}{0} \subseteq \{g \in D \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}$
10	4 9	mpdan	$⊢ φ \to X supp \underset{˙}{0} \subseteq \{g \in D \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}$

Metamath Proof Explorer