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 reldmmpl ⊢ Rel ⁡ dom ⁡ mPoly
22 21 2 3 elbasov ⊢ F ∈ B → I ∈ V ∧ R ∈ V
23 22 simprd ⊢ F ∈ B → R ∈ V
24 2 3 4 20 23 mplelsfi ⊢ F ∈ B → finSupp 0 R⁡ F
25 24 fsuppimpd ⊢ F ∈ B → F supp 0 R ∈ Fin
26 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
27 19 25 26 syl2anc ⊢ F ∈ B → b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ∈ Fin
28 27 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
29 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 ≠ ∅
30 nn0ssre ⊢ ℕ 0 ⊆ ℝ
31 ressxr ⊢ ℝ ⊆ ℝ *
32 30 31 sstri ⊢ ℕ 0 ⊆ ℝ *
33 15 32 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 ⊆ ℝ *
34 xrltso ⊢ < Or ℝ *
35 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
36 34 35 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
37 28 29 33 36 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
38 17 37 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 ∪ −∞
39 xrsup0 ⊢ sup ∅ ℝ * < = −∞
40 ssun2 ⊢ −∞ ⊆ ℕ 0 ∪ −∞
41 mnfxr ⊢ −∞ ∈ ℝ *
42 41 elexi ⊢ −∞ ∈ V
43 42 snid ⊢ −∞ ∈ −∞
44 40 43 sselii ⊢ −∞ ∈ ℕ 0 ∪ −∞
45 39 44 eqeltri ⊢ sup ∅ ℝ * < ∈ ℕ 0 ∪ −∞
46 45 a1i ⊢ F ∈ B → sup ∅ ℝ * < ∈ ℕ 0 ∪ −∞
47 9 38 46 pm2.61ne ⊢ F ∈ B → sup b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b F supp 0 R ℝ * < ∈ ℕ 0 ∪ −∞
48 7 47 eqeltrd ⊢ F ∈ B → D ⁡ F ∈ ℕ 0 ∪ −∞