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