Theorem deg1xrf

Description: Functionality of univariate polynomial degree, weak range. (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	deg1xrf	$$⊢D:B⟶{ℝ}^{*}$$

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	mdegxrf	$$⊢D:B⟶{ℝ}^{*}$$