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

Metamath Proof Explorer

Theorem mdegxrf

Description: Functionality 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 mdegxrf 
|- D : B --> 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 xrltso 
 |-  < Or RR*
5 4 supex 
 |-  sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( z supp ( 0g ` R ) ) ) , RR* , < ) e. _V
6 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
7 eqid 
 |-  { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } = { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin }
8 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 ) )
9 1 2 3 6 7 8 mdegfval 
 |-  D = ( z e. B |-> sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( z supp ( 0g ` R ) ) ) , RR* , < ) )
10 5 9 fnmpti 
 |-  D Fn B
11 1 2 3 mdegxrcl 
 |-  ( f e. B -> ( D ` f ) e. RR* )
12 11 rgen 
 |-  A. f e. B ( D ` f ) e. RR*
13 ffnfv 
 |-  ( D : B --> RR* <-> ( D Fn B /\ A. f e. B ( D ` f ) e. RR* ) )
14 10 12 13 mpbir2an 
 |-  D : B --> RR*