Theorem ismhp2

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

	Ref	Expression
Hypotheses	ismhp.h	$$⊢H=I\mathrm{mHomP}R$$
	ismhp.p	$$⊢P=I\mathrm{mPoly}R$$
	ismhp.b	$$⊢B={\mathrm{Base}}_P$$
	ismhp.0	$$⊢\underset{\dot{}}{0}=0_R$$
	ismhp.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	ismhp.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	ismhp2.1	$$⊢\phi \to X\in B$$
	ismhp2.2	$$⊢\phi \to X\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}$$
Assertion	ismhp2	$$⊢\phi \to X\in H\left(N\right)$$

Proof

Step	Hyp	Ref	Expression
1		ismhp.h	$$⊢H=I\mathrm{mHomP}R$$
2		ismhp.p	$$⊢P=I\mathrm{mPoly}R$$
3		ismhp.b	$$⊢B={\mathrm{Base}}_P$$
4		ismhp.0	$$⊢\underset{\dot{}}{0}=0_R$$
5		ismhp.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
6		ismhp.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7		ismhp2.1	$$⊢\phi \to X\in B$$
8		ismhp2.2	$$⊢\phi \to X\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}$$
9	1 2 3 4 5 6	ismhp	$$⊢\phi \to \left(X\in H\left(N\right)\leftrightarrow \left(X\in B\wedge X\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\right)$$
10	7 8 9	mpbir2and	$$⊢\phi \to X\in H\left(N\right)$$