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 mHomP R$
	mhp0cl.0	$⊢ \underset{˙}{0} = 0_{R}$
	mhp0cl.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
	mhp0cl.i	$⊢ φ \to I \in V$
	mhp0cl.r	$⊢ φ \to R \in Grp$
	mhp0cl.n	$⊢ φ \to N \in ℕ_{0}$
Assertion	mhp0cl	$⊢ φ \to D \times \{\underset{˙}{0}\} \in H (N)$

Proof

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

Metamath Proof Explorer

Theorem mhp0cl

Proof