mdeg0

Description: Degree of the zero polynomial. (Contributed by Stefan O'Rear, 20-Mar-2015) (Proof shortened by AV, 27-Jul-2019)

	Ref	Expression
Hypotheses	mdeg0.d	$⊢ D = I mDeg R$
	mdeg0.p	$⊢ P = I mPoly R$
	mdeg0.z	$⊢ \underset{˙}{0} = 0_{P}$
Assertion	mdeg0	$⊢ (I \in V \land R \in Ring) \to D (\underset{˙}{0}) = −∞$

Proof

Step	Hyp	Ref	Expression
1		mdeg0.d	$⊢ D = I mDeg R$
2		mdeg0.p	$⊢ P = I mPoly R$
3		mdeg0.z	$⊢ \underset{˙}{0} = 0_{P}$
4		ringgrp	$⊢ R \in Ring \to R \in Grp$
5	2	mplgrp	$⊢ (I \in V \land R \in Grp) \to P \in Grp$
6	4 5	sylan2	$⊢ (I \in V \land R \in Ring) \to P \in Grp$
7		eqid	$⊢ {Base}_{P} = {Base}_{P}$
8	7 3	grpidcl	$⊢ P \in Grp \to \underset{˙}{0} \in {Base}_{P}$
9		eqid	$⊢ 0_{R} = 0_{R}$
10		eqid	$⊢ \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} = \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\}$
11		eqid	$⊢ (y \in \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} y) = (y \in \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} y)$
12	1 2 7 9 10 11	mdegval	$⊢ \underset{˙}{0} \in {Base}_{P} \to D (\underset{˙}{0}) = sup ((y \in \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} y) [\underset{˙}{0} supp 0_{R}] ℝ^{*} <)$
13	6 8 12	3syl	$⊢ (I \in V \land R \in Ring) \to D (\underset{˙}{0}) = sup ((y \in \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} y) [\underset{˙}{0} supp 0_{R}] ℝ^{*} <)$
14		simpl	$⊢ (I \in V \land R \in Ring) \to I \in V$
15	4	adantl	$⊢ (I \in V \land R \in Ring) \to R \in Grp$
16	2 10 9 3 14 15	mpl0	$⊢ (I \in V \land R \in Ring) \to \underset{˙}{0} = \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} \times \{0_{R}\}$
17		fvex	$⊢ 0_{R} \in V$
18		fnconstg	$⊢ 0_{R} \in V \to (\{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} \times \{0_{R}\}) Fn \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\}$
19	17 18	mp1i	$⊢ (I \in V \land R \in Ring) \to (\{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} \times \{0_{R}\}) Fn \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\}$
20	16	fneq1d	$⊢ (I \in V \land R \in Ring) \to (\underset{˙}{0} Fn \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} \leftrightarrow (\{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} \times \{0_{R}\}) Fn \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\})$
21	19 20	mpbird	$⊢ (I \in V \land R \in Ring) \to \underset{˙}{0} Fn \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\}$
22		ovex	$⊢ {ℕ_{0}}^{I} \in V$
23	22	rabex	$⊢ \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} \in V$
24	23	a1i	$⊢ (I \in V \land R \in Ring) \to \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} \in V$
25	17	a1i	$⊢ (I \in V \land R \in Ring) \to 0_{R} \in V$
26		fnsuppeq0	$⊢ (\underset{˙}{0} Fn \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} \land \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} \in V \land 0_{R} \in V) \to (\underset{˙}{0} supp 0_{R} = \emptyset \leftrightarrow \underset{˙}{0} = \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} \times \{0_{R}\})$
27	21 24 25 26	syl3anc	$⊢ (I \in V \land R \in Ring) \to (\underset{˙}{0} supp 0_{R} = \emptyset \leftrightarrow \underset{˙}{0} = \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} \times \{0_{R}\})$
28	16 27	mpbird	$⊢ (I \in V \land R \in Ring) \to \underset{˙}{0} supp 0_{R} = \emptyset$
29	28	imaeq2d	$⊢ (I \in V \land R \in Ring) \to (y \in \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} y) [\underset{˙}{0} supp 0_{R}] = (y \in \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} y) [\emptyset]$
30		ima0	$⊢ (y \in \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} y) [\emptyset] = \emptyset$
31	29 30	eqtrdi	$⊢ (I \in V \land R \in Ring) \to (y \in \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} y) [\underset{˙}{0} supp 0_{R}] = \emptyset$
32	31	supeq1d	$⊢ (I \in V \land R \in Ring) \to sup ((y \in \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} y) [\underset{˙}{0} supp 0_{R}] ℝ^{} <) = sup (\emptyset ℝ^{} <)$
33		xrsup0	$⊢ sup (\emptyset ℝ^{*} <) = −∞$
34	32 33	eqtrdi	$⊢ (I \in V \land R \in Ring) \to sup ((y \in \{x \in ({ℕ_{0}}^{I}) \| x^{-1} [ℕ] \in Fin\} ⟼ \sum_{ℂ_{fld}} y) [\underset{˙}{0} supp 0_{R}] ℝ^{*} <) = −∞$
35	13 34	eqtrd	$⊢ (I \in V \land R \in Ring) \to D (\underset{˙}{0}) = −∞$

Metamath Proof Explorer

Theorem mdeg0

Proof