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 2 3 mplrcl 
 |-  ( F e. B -> I e. _V )
12 5 6 tdeglem1 
 |-  ( I e. _V -> ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) : { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } --> NN0 )
13 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 )
14 11 12 13 3syl 
 |-  ( F e. B -> ran ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) C_ NN0 )
15 10 14 sstrid 
 |-  ( F e. B -> ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) C_ NN0 )
16 15 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 )
17 ssun1 
 |-  NN0 C_ ( NN0 u. { -oo } )
18 16 17 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 } ) )
19 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 ) ) )
20 11 12 19 3syl 
 |-  ( F e. B -> Fun ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) )
21 id 
 |-  ( F e. B -> F e. B )
22 reldmmpl 
 |-  Rel dom mPoly
23 22 2 3 elbasov 
 |-  ( F e. B -> ( I e. _V /\ R e. _V ) )
24 23 simprd 
 |-  ( F e. B -> R e. _V )
25 2 3 4 21 24 mplelsfi 
 |-  ( F e. B -> F finSupp ( 0g ` R ) )
26 25 fsuppimpd 
 |-  ( F e. B -> ( F supp ( 0g ` R ) ) e. Fin )
27 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 )
28 20 26 27 syl2anc 
 |-  ( F e. B -> ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( F supp ( 0g ` R ) ) ) e. Fin )
29 28 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 )
30 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 ) ) ) =/= (/) )
31 nn0ssre 
 |-  NN0 C_ RR
32 ressxr 
 |-  RR C_ RR*
33 31 32 sstri 
 |-  NN0 C_ RR*
34 16 33 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* )
35 xrltso 
 |-  < Or RR*
36 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 ) ) ) )
37 35 36 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 ) ) ) )
38 29 30 34 37 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 ) ) ) )
39 18 38 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 } ) )
40 xrsup0 
 |-  sup ( (/) , RR* , < ) = -oo
41 ssun2 
 |-  { -oo } C_ ( NN0 u. { -oo } )
42 mnfxr 
 |-  -oo e. RR*
43 42 elexi 
 |-  -oo e. _V
44 43 snid 
 |-  -oo e. { -oo }
45 41 44 sselii 
 |-  -oo e. ( NN0 u. { -oo } )
46 40 45 eqeltri 
 |-  sup ( (/) , RR* , < ) e. ( NN0 u. { -oo } )
47 46 a1i 
 |-  ( F e. B -> sup ( (/) , RR* , < ) e. ( NN0 u. { -oo } ) )
48 9 39 47 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 } ) )
49 7 48 eqeltrd 
 |-  ( F e. B -> ( D ` F ) e. ( NN0 u. { -oo } ) )