Theorem deg1xrcl

Description: Closure of univariate polynomial degree in extended reals. (Contributed by Stefan O'Rear, 23-Mar-2015)

	Ref	Expression
Hypotheses	deg1xrf.d	|- D = ( deg1 ` R )
	deg1xrf.p	|- P = ( Poly1 ` R )
	deg1xrf.b	|- B = ( Base ` P )
Assertion	deg1xrcl	|- ( F e. B -> ( D ` F ) e. RR* )

Proof

Step	Hyp	Ref	Expression
1		deg1xrf.d	|- D = ( deg1 ` R )
2		deg1xrf.p	|- P = ( Poly1 ` R )
3		deg1xrf.b	|- B = ( Base ` P )
4	1 2 3	deg1xrf	|- D : B --> RR*
5	4	ffvelrni	|- ( F e. B -> ( D ` F ) e. RR* )