Theorem deg1xrf

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

	Ref	Expression
Hypotheses	deg1xrf.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1xrf.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1xrf.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
Assertion	deg1xrf	⊢ 𝐷 : 𝐵 ⟶ ℝ*

Proof

Step	Hyp	Ref	Expression
1		deg1xrf.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1xrf.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		deg1xrf.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4	1	deg1fval	⊢ 𝐷 = ( 1o mDeg 𝑅 )
5		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
6		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
7	2 6 3	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
8	4 5 7	mdegxrf	⊢ 𝐷 : 𝐵 ⟶ ℝ*