Metamath Proof Explorer

Theorem mdegcl

Description: Sharp closure for multivariate polynomials. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses mdegcl.d ⊢ D = I mDeg R
mdegcl.p ⊢ P = I mPoly R
mdegcl.b ⊢ B = Base P
Assertion mdegcl ⊢ F ∈ B → D ⁡ F ∈ ℕ 0 ∪ −∞

Proof

Step Hyp Ref Expression
1 mdegcl.d ⊢ D = I mDeg R
2 mdegcl.p ⊢ P = I mPoly R
3 mdegcl.b ⊢ B = Base P
4 eqid ⊢ 0 R = 0 R
5 eqid ⊢ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin = a ∈ ℕ 0 I | a -1 ℕ ∈ Fin
6 eqid ⊢ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b = b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b
7 1 2 3 4 5 6 mdegval ⊢ F ∈ B → D ⁡ F = sup b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ℝ * <
8 supeq1 ⊢ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R = ∅ → sup b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ℝ * < = sup ∅ ℝ * <
9 8 eleq1d ⊢ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R = ∅ → sup b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ℝ * < ∈ ℕ 0 ∪ −∞ ↔ sup ∅ ℝ * < ∈ ℕ 0 ∪ −∞
10 imassrn ⊢ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ⊆ ran ⁡ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b
11 5 6 tdeglem1 ⊢ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b : a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟶ ℕ 0
12 frn ⊢ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b : a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟶ ℕ 0 → ran ⁡ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b ⊆ ℕ 0
13 11 12 mp1i ⊢ F ∈ B → ran ⁡ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b ⊆ ℕ 0
14 10 13 sstrid ⊢ F ∈ B → b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ⊆ ℕ 0
15 14 adantr ⊢ F ∈ B ∧ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ≠ ∅ → b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ⊆ ℕ 0
16 ssun1 ⊢ ℕ 0 ⊆ ℕ 0 ∪ −∞
17 15 16 sstrdi ⊢ F ∈ B ∧ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ≠ ∅ → b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ⊆ ℕ 0 ∪ −∞
18 ffun ⊢ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b : a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟶ ℕ 0 → Fun ⁡ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b
19 11 18 mp1i ⊢ F ∈ B → Fun ⁡ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b
20 id ⊢ F ∈ B → F ∈ B
21 2 3 4 20 mplelsfi ⊢ F ∈ B → finSupp 0 R⁡ F
22 21 fsuppimpd ⊢ F ∈ B → F supp 0 R ∈ Fin
23 imafi ⊢ Fun ⁡ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b ∧ F supp 0 R ∈ Fin → b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ∈ Fin
24 19 22 23 syl2anc ⊢ F ∈ B → b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ∈ Fin
25 24 adantr ⊢ F ∈ B ∧ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ≠ ∅ → b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ∈ Fin
26 simpr ⊢ F ∈ B ∧ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ≠ ∅ → b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ≠ ∅
27 nn0ssre ⊢ ℕ 0 ⊆ ℝ
28 ressxr ⊢ ℝ ⊆ ℝ *
29 27 28 sstri ⊢ ℕ 0 ⊆ ℝ *
30 15 29 sstrdi ⊢ F ∈ B ∧ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ≠ ∅ → b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ⊆ ℝ *
31 xrltso ⊢ < Or ℝ *
32 fisupcl ⊢ < Or ℝ * ∧ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ∈ Fin ∧ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ≠ ∅ ∧ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ⊆ ℝ * → sup b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ℝ * < ∈ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R
33 31 32 mpan ⊢ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ∈ Fin ∧ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ≠ ∅ ∧ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ⊆ ℝ * → sup b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ℝ * < ∈ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R
34 25 26 30 33 syl3anc ⊢ F ∈ B ∧ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ≠ ∅ → sup b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ℝ * < ∈ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R
35 17 34 sseldd ⊢ F ∈ B ∧ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ≠ ∅ → sup b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ℝ * < ∈ ℕ 0 ∪ −∞
36 xrsup0 ⊢ sup ∅ ℝ * < = −∞
37 ssun2 ⊢ −∞ ⊆ ℕ 0 ∪ −∞
38 mnfxr ⊢ −∞ ∈ ℝ *
39 38 elexi ⊢ −∞ ∈ V
40 39 snid ⊢ −∞ ∈ −∞
41 37 40 sselii ⊢ −∞ ∈ ℕ 0 ∪ −∞
42 36 41 eqeltri ⊢ sup ∅ ℝ * < ∈ ℕ 0 ∪ −∞
43 42 a1i ⊢ F ∈ B → sup ∅ ℝ * < ∈ ℕ 0 ∪ −∞
44 9 35 43 pm2.61ne ⊢ F ∈ B → sup b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ℝ * < ∈ ℕ 0 ∪ −∞
45 7 44 eqeltrd ⊢ F ∈ B → D ⁡ F ∈ ℕ 0 ∪ −∞