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 *

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 *
5 4 supex sup y x 0 I | x -1 Fin fld y z supp 0 R * < V
6 eqid 0 R = 0 R
7 eqid x 0 I | x -1 Fin = x 0 I | x -1 Fin
8 eqid y x 0 I | x -1 Fin fld y = y x 0 I | x -1 Fin fld y
9 1 2 3 6 7 8 mdegfval D = z B sup y x 0 I | x -1 Fin fld y z supp 0 R * <
10 5 9 fnmpti D Fn B
11 1 2 3 mdegxrcl f B D f *
12 11 rgen f B D f *
13 ffnfv D : B * D Fn B f B D f *
14 10 12 13 mpbir2an D : B *