Theorem deg1cl

Description: Sharp closure of univariate polynomial degree. (Contributed by Stefan O'Rear, 23-Mar-2015)

	Ref	Expression
Hypotheses	deg1xrf.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	deg1xrf.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	deg1xrf.b	$$⊢B={\mathrm{Base}}_P$$
Assertion	deg1cl	$$⊢F\in B\to D\left(F\right)\in \left({\mathbb{N}}_0\cup \left\{\mathrm{-\infty }\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		deg1xrf.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
2		deg1xrf.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		deg1xrf.b	$$⊢B={\mathrm{Base}}_P$$
4	1	deg1fval	$$⊢D=1_{𝑜}\mathrm{mDeg}R$$
5		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
6		eqid	$$⊢{\mathrm{PwSer}}_1\left(R\right)={\mathrm{PwSer}}_1\left(R\right)$$
7	2 6 3	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
8	4 5 7	mdegcl	$$⊢F\in B\to D\left(F\right)\in \left({\mathbb{N}}_0\cup \left\{\mathrm{-\infty }\right\}\right)$$