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*