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 e. B -> ( D ` F ) e. ( NN0 u. { -oo } ) )

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 
 |-  ( 0g ` R ) = ( 0g ` R )
5 eqid 
 |-  { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } = { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin }
6 eqid 
 |-  ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) = ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) )
7 1 2 3 4 5 6 mdegval 
 |-  ( F e. B -> ( D ` F ) = sup ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) , RR* , < ) )
8 supeq1 
 |-  ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) = (/) -> sup ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) , RR* , < ) = sup ( (/) , RR* , < ) )
9 8 eleq1d 
 |-  ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) = (/) -> ( sup ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) , RR* , < ) e. ( NN0 u. { -oo } ) <-> sup ( (/) , RR* , < ) e. ( NN0 u. { -oo } ) ) )
10 imassrn 
 |-  ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) C_ ran ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) )
11 5 6 tdeglem1 
 |-  ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) : { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } --> NN0
12 frn 
 |-  ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) : { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } --> NN0 -> ran ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) C_ NN0 )
13 11 12 mp1i 
 |-  ( F e. B -> ran ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) C_ NN0 )
14 10 13 sstrid 
 |-  ( F e. B -> ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) C_ NN0 )
15 14 adantr 
 |-  ( ( F e. B /\ ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) =/= (/) ) -> ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) C_ NN0 )
16 ssun1 
 |-  NN0 C_ ( NN0 u. { -oo } )
17 15 16 sstrdi 
 |-  ( ( F e. B /\ ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) =/= (/) ) -> ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) C_ ( NN0 u. { -oo } ) )
18 ffun 
 |-  ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) : { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } --> NN0 -> Fun ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) )
19 11 18 mp1i 
 |-  ( F e. B -> Fun ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) )
20 id 
 |-  ( F e. B -> F e. B )
21 2 3 4 20 mplelsfi 
 |-  ( F e. B -> F finSupp ( 0g ` R ) )
22 21 fsuppimpd 
 |-  ( F e. B -> ( F supp ( 0g ` R ) ) e. Fin )
23 imafi 
 |-  ( ( Fun ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) /\ ( F supp ( 0g ` R ) ) e. Fin ) -> ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) e. Fin )
24 19 22 23 syl2anc 
 |-  ( F e. B -> ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) e. Fin )
25 24 adantr 
 |-  ( ( F e. B /\ ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) =/= (/) ) -> ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) e. Fin )
26 simpr 
 |-  ( ( F e. B /\ ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) =/= (/) ) -> ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) =/= (/) )
27 nn0ssre 
 |-  NN0 C_ RR
28 ressxr 
 |-  RR C_ RR*
29 27 28 sstri 
 |-  NN0 C_ RR*
30 15 29 sstrdi 
 |-  ( ( F e. B /\ ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) =/= (/) ) -> ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) C_ RR* )
31 xrltso 
 |-  < Or RR*
32 fisupcl 
 |-  ( ( < Or RR* /\ ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) e. Fin /\ ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) =/= (/) /\ ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) C_ RR* ) ) -> sup ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) , RR* , < ) e. ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) )
33 31 32 mpan 
 |-  ( ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) e. Fin /\ ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) =/= (/) /\ ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) C_ RR* ) -> sup ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) , RR* , < ) e. ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) )
34 25 26 30 33 syl3anc 
 |-  ( ( F e. B /\ ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) =/= (/) ) -> sup ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) , RR* , < ) e. ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) )
35 17 34 sseldd 
 |-  ( ( F e. B /\ ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) =/= (/) ) -> sup ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) , RR* , < ) e. ( NN0 u. { -oo } ) )
36 xrsup0 
 |-  sup ( (/) , RR* , < ) = -oo
37 ssun2 
 |-  { -oo } C_ ( NN0 u. { -oo } )
38 mnfxr 
 |-  -oo e. RR*
39 38 elexi 
 |-  -oo e. _V
40 39 snid 
 |-  -oo e. { -oo }
41 37 40 sselii 
 |-  -oo e. ( NN0 u. { -oo } )
42 36 41 eqeltri 
 |-  sup ( (/) , RR* , < ) e. ( NN0 u. { -oo } )
43 42 a1i 
 |-  ( F e. B -> sup ( (/) , RR* , < ) e. ( NN0 u. { -oo } ) )
44 9 35 43 pm2.61ne 
 |-  ( F e. B -> sup ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) , RR* , < ) e. ( NN0 u. { -oo } ) )
45 7 44 eqeltrd 
 |-  ( F e. B -> ( D ` F ) e. ( NN0 u. { -oo } ) )