Theorem ismhp3

Description: A polynomial is homogeneous iff the degree of every nonzero term is the same. (Contributed by SN, 22-Jul-2024)

	Ref	Expression
Hypotheses	mhpfval.h	$$⊢H=I\mathrm{mHomP}R$$
	mhpfval.p	$$⊢P=I\mathrm{mPoly}R$$
	mhpfval.b	$$⊢B={\mathrm{Base}}_P$$
	mhpfval.0	$$⊢\underset{\dot{}}{0}=0_R$$
	mhpfval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mhpfval.i	$$⊢\phi \to I\in V$$
	mhpfval.r	$$⊢\phi \to R\in W$$
	mhpval.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	ismhp2.1	$$⊢\phi \to X\in B$$
Assertion	ismhp3	$$⊢\phi \to \left(X\in H\left(N\right)\leftrightarrow \forall d\in D\left(X\left(d\right)\ne \underset{\dot{}}{0}\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=N\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mhpfval.h	$$⊢H=I\mathrm{mHomP}R$$
2		mhpfval.p	$$⊢P=I\mathrm{mPoly}R$$
3		mhpfval.b	$$⊢B={\mathrm{Base}}_P$$
4		mhpfval.0	$$⊢\underset{\dot{}}{0}=0_R$$
5		mhpfval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
6		mhpfval.i	$$⊢\phi \to I\in V$$
7		mhpfval.r	$$⊢\phi \to R\in W$$
8		mhpval.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
9		ismhp2.1	$$⊢\phi \to X\in B$$
10	1 2 3 4 5 6 7 8	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)$$
11	9	biantrurd	$$⊢\phi \to \left(X\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=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)$$
12		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
13	2 12 3 5 9	mplelf	$$⊢\phi \to X:D⟶{\mathrm{Base}}_R$$
14	13	ffnd	$$⊢\phi \to XFnD$$
15	4	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
16	15	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
17		elsuppfng	$$⊢\left(XFnD\wedge X\in B\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)\to \left(d\in {supp}_{\underset{\dot{}}{0}}\left(X\right)\leftrightarrow \left(d\in D\wedge X\left(d\right)\ne \underset{\dot{}}{0}\right)\right)$$
18	14 9 16 17	syl3anc	$$⊢\phi \to \left(d\in {supp}_{\underset{\dot{}}{0}}\left(X\right)\leftrightarrow \left(d\in D\wedge X\left(d\right)\ne \underset{\dot{}}{0}\right)\right)$$
19		oveq2	$$⊢g=d\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g={\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d$$
20	19	eqeq1d	$$⊢g=d\to \left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\leftrightarrow {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=N\right)$$
21	20	elrab	$$⊢d\in \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\leftrightarrow \left(d\in D\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=N\right)$$
22	21	a1i	$$⊢\phi \to \left(d\in \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\leftrightarrow \left(d\in D\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=N\right)\right)$$
23	18 22	imbi12d	$$⊢\phi \to \left(\left(d\in {supp}_{\underset{\dot{}}{0}}\left(X\right)\to d\in \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\leftrightarrow \left(\left(d\in D\wedge X\left(d\right)\ne \underset{\dot{}}{0}\right)\to \left(d\in D\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=N\right)\right)\right)$$
24		imdistan	$$⊢\left(d\in D\to \left(X\left(d\right)\ne \underset{\dot{}}{0}\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=N\right)\right)\leftrightarrow \left(\left(d\in D\wedge X\left(d\right)\ne \underset{\dot{}}{0}\right)\to \left(d\in D\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=N\right)\right)$$
25	23 24	bitr4di	$$⊢\phi \to \left(\left(d\in {supp}_{\underset{\dot{}}{0}}\left(X\right)\to d\in \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\leftrightarrow \left(d\in D\to \left(X\left(d\right)\ne \underset{\dot{}}{0}\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=N\right)\right)\right)$$
26	25	albidv	$$⊢\phi \to \left(\forall d\left(d\in {supp}_{\underset{\dot{}}{0}}\left(X\right)\to d\in \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)\leftrightarrow \forall d\left(d\in D\to \left(X\left(d\right)\ne \underset{\dot{}}{0}\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=N\right)\right)\right)$$
27		dfss2	$$⊢X\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\leftrightarrow \forall d\left(d\in {supp}_{\underset{\dot{}}{0}}\left(X\right)\to d\in \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\right)$$
28		df-ral	$$⊢\forall d\in D\left(X\left(d\right)\ne \underset{\dot{}}{0}\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=N\right)\leftrightarrow \forall d\left(d\in D\to \left(X\left(d\right)\ne \underset{\dot{}}{0}\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=N\right)\right)$$
29	26 27 28	3bitr4g	$$⊢\phi \to \left(X\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\leftrightarrow \forall d\in D\left(X\left(d\right)\ne \underset{\dot{}}{0}\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=N\right)\right)$$
30	10 11 29	3bitr2d	$$⊢\phi \to \left(X\in H\left(N\right)\leftrightarrow \forall d\in D\left(X\left(d\right)\ne \underset{\dot{}}{0}\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}d=N\right)\right)$$