Theorem mhp0cl

Description: The zero polynomial is homogeneous. (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	$$⊢0_{\left(I\mathrm{mPoly}R\right)}=0_{\left(I\mathrm{mPoly}R\right)}$$
9	7 3 2 8 4 5	mpl0	$$⊢\phi \to 0_{\left(I\mathrm{mPoly}R\right)}=D\times \left\{\underset{\dot{}}{0}\right\}$$
10	7	mplgrp	$$⊢\left(I\in V\wedge R\in \mathrm{Grp}\right)\to I\mathrm{mPoly}R\in \mathrm{Grp}$$
11	4 5 10	syl2anc	$$⊢\phi \to I\mathrm{mPoly}R\in \mathrm{Grp}$$
12		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
13	12 8	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	11 13	syl	$$⊢\phi \to 0_{\left(I\mathrm{mPoly}R\right)}\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
15	9 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	16	a1i	$$⊢\phi \to \left(D\times \left\{\underset{\dot{}}{0}\right\}\right)\mathrm{supp}\underset{\dot{}}{0}=\varnothing$$
18		0ss	$$⊢\varnothing \subseteq \left\{g\in D|\sum _{j\in {\mathbb{N}}_0}g\left(j\right)=N\right\}$$
19	17 18	eqsstrdi	$$⊢\phi \to \left(D\times \left\{\underset{\dot{}}{0}\right\}\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|\sum _{j\in {\mathbb{N}}_0}g\left(j\right)=N\right\}$$
20	1 7 12 2 3 4 5 6	ismhp	$$⊢\phi \to \left(D\times \left\{\underset{\dot{}}{0}\right\}\in H\left(N\right)\leftrightarrow \left(D\times \left\{\underset{\dot{}}{0}\right\}\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}\wedge \left(D\times \left\{\underset{\dot{}}{0}\right\}\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{g\in D|\sum _{j\in {\mathbb{N}}_0}g\left(j\right)=N\right\}\right)\right)$$
21	15 19 20	mpbir2and	$$⊢\phi \to D\times \left\{\underset{\dot{}}{0}\right\}\in H\left(N\right)$$