Metamath Proof Explorer

Theorem mdegxrcl

Description: Closure of polynomial degree in the extended reals. (Contributed by Stefan O'Rear, 19-Mar-2015) (Proof shortened by AV, 27-Jul-2019)

Ref Expression
Hypotheses mdegxrcl.d 
|- D = ( I mDeg R )
mdegxrcl.p 
|- P = ( I mPoly R )
mdegxrcl.b 
|- B = ( Base ` P )
Assertion mdegxrcl 
|- ( F e. B -> ( D ` F ) e. RR* )

Proof

Step Hyp Ref Expression
1 mdegxrcl.d 
 |-  D = ( I mDeg R )
2 mdegxrcl.p 
 |-  P = ( I mPoly R )
3 mdegxrcl.b 
 |-  B = ( Base ` P )
4 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
5 eqid 
 |-  { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } = { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin }
6 eqid 
 |-  ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) = ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) )
7 1 2 3 4 5 6 mdegval 
 |-  ( F e. B -> ( D ` F ) = sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( F supp ( 0g ` R ) ) ) , RR* , < ) )
8 imassrn 
 |-  ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( F supp ( 0g ` R ) ) ) C_ ran ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) )
9 2 3 mplrcl 
 |-  ( F e. B -> I e. _V )
10 5 6 tdeglem1 
 |-  ( I e. _V -> ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) : { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } --> NN0 )
11 frn 
 |-  ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) : { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } --> NN0 -> ran ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) C_ NN0 )
12 9 10 11 3syl 
 |-  ( F e. B -> ran ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) C_ NN0 )
13 nn0ssre 
 |-  NN0 C_ RR
14 ressxr 
 |-  RR C_ RR*
15 13 14 sstri 
 |-  NN0 C_ RR*
16 12 15 sstrdi 
 |-  ( F e. B -> ran ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) C_ RR* )
17 8 16 sstrid 
 |-  ( F e. B -> ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( F supp ( 0g ` R ) ) ) C_ RR* )
18 supxrcl 
 |-  ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( F supp ( 0g ` R ) ) ) C_ RR* -> sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( F supp ( 0g ` R ) ) ) , RR* , < ) e. RR* )
19 17 18 syl 
 |-  ( F e. B -> sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( F supp ( 0g ` R ) ) ) , RR* , < ) e. RR* )
20 7 19 eqeltrd 
 |-  ( F e. B -> ( D ` F ) e. RR* )