Metamath Proof Explorer

Theorem 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 ⊢ 0 ˙ = 0 P
Assertion mdeg0 ⊢ I ∈ V ∧ R ∈ Ring → D ⁡ 0 ˙ = −∞

Proof

Step Hyp Ref Expression
1 mdeg0.d ⊢ D = I mDeg R
2 mdeg0.p ⊢ P = I mPoly R
3 mdeg0.z ⊢ 0 ˙ = 0 P
4 ringgrp ⊢ R ∈ Ring → R ∈ Grp
5 2 mplgrp ⊢ I ∈ V ∧ R ∈ Grp → P ∈ Grp
6 4 5 sylan2 ⊢ I ∈ V ∧ R ∈ Ring → P ∈ Grp
7 eqid ⊢ Base P = Base P
8 7 3 grpidcl ⊢ P ∈ Grp → 0 ˙ ∈ Base P
9 eqid ⊢ 0 R = 0 R
10 eqid ⊢ x ∈ ℕ 0 I | x -1 ℕ ∈ Fin = x ∈ ℕ 0 I | x -1 ℕ ∈ Fin
11 eqid ⊢ y ∈ x ∈ ℕ 0 I | x -1 ℕ ∈ Fin ⟼ ∑ ℂ fld y = y ∈ x ∈ ℕ 0 I | x -1 ℕ ∈ Fin ⟼ ∑ ℂ fld y
12 1 2 7 9 10 11 mdegval ⊢ 0 ˙ ∈ Base P → D ⁡ 0 ˙ = sup y ∈ x ∈ ℕ 0 I | x -1 ℕ ∈ Fin ⟼ ∑ ℂ fld y 0 ˙ supp 0 R ℝ * <
13 6 8 12 3syl ⊢ I ∈ V ∧ R ∈ Ring → D ⁡ 0 ˙ = sup y ∈ x ∈ ℕ 0 I | x -1 ℕ ∈ Fin ⟼ ∑ ℂ fld y 0 ˙ supp 0 R ℝ * <
14 simpl ⊢ I ∈ V ∧ R ∈ Ring → I ∈ V
15 4 adantl ⊢ I ∈ V ∧ R ∈ Ring → R ∈ Grp
16 2 10 9 3 14 15 mpl0 ⊢ I ∈ V ∧ R ∈ Ring → 0 ˙ = x ∈ ℕ 0 I | x -1 ℕ ∈ Fin × 0 R
17 fvex ⊢ 0 R ∈ V
18 fnconstg ⊢ 0 R ∈ V → x ∈ ℕ 0 I | x -1 ℕ ∈ Fin × 0 R Fn x ∈ ℕ 0 I | x -1 ℕ ∈ Fin
19 17 18 mp1i ⊢ I ∈ V ∧ R ∈ Ring → x ∈ ℕ 0 I | x -1 ℕ ∈ Fin × 0 R Fn x ∈ ℕ 0 I | x -1 ℕ ∈ Fin
20 16 fneq1d ⊢ I ∈ V ∧ R ∈ Ring → 0 ˙ Fn x ∈ ℕ 0 I | x -1 ℕ ∈ Fin ↔ x ∈ ℕ 0 I | x -1 ℕ ∈ Fin × 0 R Fn x ∈ ℕ 0 I | x -1 ℕ ∈ Fin
21 19 20 mpbird ⊢ I ∈ V ∧ R ∈ Ring → 0 ˙ Fn x ∈ ℕ 0 I | x -1 ℕ ∈ Fin
22 ovex ⊢ ℕ 0 I ∈ V
23 22 rabex ⊢ x ∈ ℕ 0 I | x -1 ℕ ∈ Fin ∈ V
24 23 a1i ⊢ I ∈ V ∧ R ∈ Ring → x ∈ ℕ 0 I | x -1 ℕ ∈ Fin ∈ V
25 17 a1i ⊢ I ∈ V ∧ R ∈ Ring → 0 R ∈ V
26 fnsuppeq0 ⊢ 0 ˙ Fn x ∈ ℕ 0 I | x -1 ℕ ∈ Fin ∧ x ∈ ℕ 0 I | x -1 ℕ ∈ Fin ∈ V ∧ 0 R ∈ V → 0 ˙ supp 0 R = ∅ ↔ 0 ˙ = x ∈ ℕ 0 I | x -1 ℕ ∈ Fin × 0 R
27 21 24 25 26 syl3anc ⊢ I ∈ V ∧ R ∈ Ring → 0 ˙ supp 0 R = ∅ ↔ 0 ˙ = x ∈ ℕ 0 I | x -1 ℕ ∈ Fin × 0 R
28 16 27 mpbird ⊢ I ∈ V ∧ R ∈ Ring → 0 ˙ supp 0 R = ∅
29 28 imaeq2d ⊢ I ∈ V ∧ R ∈ Ring → y ∈ x ∈ ℕ 0 I | x -1 ℕ ∈ Fin ⟼ ∑ ℂ fld y 0 ˙ supp 0 R = y ∈ x ∈ ℕ 0 I | x -1 ℕ ∈ Fin ⟼ ∑ ℂ fld y ∅
30 ima0 ⊢ y ∈ x ∈ ℕ 0 I | x -1 ℕ ∈ Fin ⟼ ∑ ℂ fld y ∅ = ∅
31 29 30 syl6eq ⊢ I ∈ V ∧ R ∈ Ring → y ∈ x ∈ ℕ 0 I | x -1 ℕ ∈ Fin ⟼ ∑ ℂ fld y 0 ˙ supp 0 R = ∅
32 31 supeq1d ⊢ I ∈ V ∧ R ∈ Ring → sup y ∈ x ∈ ℕ 0 I | x -1 ℕ ∈ Fin ⟼ ∑ ℂ fld y 0 ˙ supp 0 R ℝ * < = sup ∅ ℝ * <
33 xrsup0 ⊢ sup ∅ ℝ * < = −∞
34 32 33 syl6eq ⊢ I ∈ V ∧ R ∈ Ring → sup y ∈ x ∈ ℕ 0 I | x -1 ℕ ∈ Fin ⟼ ∑ ℂ fld y 0 ˙ supp 0 R ℝ * < = −∞
35 13 34 eqtrd ⊢ I ∈ V ∧ R ∈ Ring → D ⁡ 0 ˙ = −∞