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 5 6 tdeglem1
 |-  ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) : { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } --> NN0
10 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 )
11 9 10 mp1i
 |-  ( F e. B -> ran ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) C_ NN0 )
12 nn0ssre
 |-  NN0 C_ RR
13 ressxr
 |-  RR C_ RR*
14 12 13 sstri
 |-  NN0 C_ RR*
15 11 14 sstrdi
 |-  ( F e. B -> ran ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) C_ RR* )
16 8 15 sstrid
 |-  ( F e. B -> ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( F supp ( 0g ` R ) ) ) C_ RR* )
17 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* )
18 16 17 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* )
19 7 18 eqeltrd
 |-  ( F e. B -> ( D ` F ) e. RR* )