ismhp2

Description: Deduce a homogeneous polynomial from its properties. (Contributed by SN, 25-May-2024)

	Ref	Expression
Hypotheses	ismhp.h	$⊢ H = I mHomP R$
	ismhp.p	$⊢ P = I mPoly R$
	ismhp.b	$⊢ B = {Base}_{P}$
	ismhp.0	$⊢ \underset{˙}{0} = 0_{R}$
	ismhp.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
	ismhp.n	$⊢ φ \to N \in ℕ_{0}$
	ismhp2.1	$⊢ φ \to X \in B$
	ismhp2.2	$⊢ φ \to X supp \underset{˙}{0} \subseteq \{g \in D \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}$
Assertion	ismhp2	$⊢ φ \to X \in H (N)$

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

Metamath Proof Explorer