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 −∞