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=ImDegR
mdegxrcl.p P=ImPolyR
mdegxrcl.b B=BaseP
Assertion mdegxrf D:B*

Proof

Step Hyp Ref Expression
1 mdegxrcl.d D=ImDegR
2 mdegxrcl.p P=ImPolyR
3 mdegxrcl.b B=BaseP
4 xrltso <Or*
5 4 supex supyx0I|x-1Finfldyzsupp0R*<V
6 eqid 0R=0R
7 eqid x0I|x-1Fin=x0I|x-1Fin
8 eqid yx0I|x-1Finfldy=yx0I|x-1Finfldy
9 1 2 3 6 7 8 mdegfval D=zBsupyx0I|x-1Finfldyzsupp0R*<
10 5 9 fnmpti DFnB
11 1 2 3 mdegxrcl fBDf*
12 11 rgen fBDf*
13 ffnfv D:B*DFnBfBDf*
14 10 12 13 mpbir2an D:B*