This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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* )