Theorem mhp0cl

Description: The zero polynomial is homogeneous. Under df-mhp , it has any (nonnegative integer) degree which loosely corresponds to the value "undefined". The values -oo and 0 are also used in Metamath (by df-mdeg and df-dgr respectively) and the literature: https://math.stackexchange.com/a/1796314/593843 . (Contributed by SN, 12-Sep-2023)

	Ref	Expression
Hypotheses	mhp0cl.h	$$⊢H=I\mathrm{mHomP}R$$
	mhp0cl.0	$$⊢\underset{\dot{}}{0}=0_R$$
	mhp0cl.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mhp0cl.i	$$⊢\phi \to I\in V$$
	mhp0cl.r	$$⊢\phi \to R\in \mathrm{Grp}$$
	mhp0cl.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	mhp0cl	$$⊢\phi \to D\times \left\{\underset{\dot{}}{0}\right\}\in H\left(N\right)$$

Proof

Step	Hyp	Ref	Expression
1		mhp0cl.h	$$⊢H=I\mathrm{mHomP}R$$
2		mhp0cl.0	$$⊢\underset{\dot{}}{0}=0_R$$
3		mhp0cl.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
4		mhp0cl.i	$$⊢\phi \to I\in V$$
5		mhp0cl.r	$$⊢\phi \to R\in \mathrm{Grp}$$
6		mhp0cl.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7		eqid	$$⊢I\mathrm{mPoly}R=I\mathrm{mPoly}R$$
8		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
9		eqid	$$⊢0_{\left(I\mathrm{mPoly}R\right)}=0_{\left(I\mathrm{mPoly}R\right)}$$
10	7 3 2 9 4 5	mpl0	$$⊢\phi \to 0_{\left(I\mathrm{mPoly}R\right)}=D\times \left\{\underset{\dot{}}{0}\right\}$$
11	7	mplgrp	$$⊢\left(I\in V\wedge R\in \mathrm{Grp}\right)\to I\mathrm{mPoly}R\in \mathrm{Grp}$$
12	4 5 11	syl2anc	$$⊢\phi \to I\mathrm{mPoly}R\in \mathrm{Grp}$$
13	8 9	grpidcl	$$⊢I\mathrm{mPoly}R\in \mathrm{Grp}\to 0_{\left(I\mathrm{mPoly}R\right)}\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
14	12 13	syl	$$⊢\phi \to 0_{\left(I\mathrm{mPoly}R\right)}\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
15	10 14	eqeltrrd	$$⊢\phi \to D\times \left\{\underset{\dot{}}{0}\right\}\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
16		fczsupp0	$$⊢\left(D\times \left\{\underset{\dot{}}{0}\right\}\right)\mathrm{supp}\underset{\dot{}}{0}=\varnothing$$
17		0ss	$$⊢\varnothing \subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}$$
18	16 17	eqsstri	$$⊢\left(D\times \left\{\underset{\dot{}}{0}\right\}\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}$$
19	18	a1i	$$⊢\phi \to \left(D\times \left\{\underset{\dot{}}{0}\right\}\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}$$
20	1 7 8 2 3 4 5 6 15 19	ismhp2	$$⊢\phi \to D\times \left\{\underset{\dot{}}{0}\right\}\in H\left(N\right)$$