Theorem deg1cl

Description: Sharp closure of univariate polynomial degree. (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	deg1cl	|- ( F e. B -> ( D ` F ) e. ( NN0 u. { -oo } ) )

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	deg1fval	|- D = ( 1o mDeg R )
5		eqid	|- ( 1o mPoly R ) = ( 1o mPoly R )
6		eqid	|- ( PwSer1 ` R ) = ( PwSer1 ` R )
7	2 6 3	ply1bas	|- B = ( Base ` ( 1o mPoly R ) )
8	4 5 7	mdegcl	|- ( F e. B -> ( D ` F ) e. ( NN0 u. { -oo } ) )