This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 2 3 ply1bas ⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
7 4 5 6 mdegxrf ⊢ 𝐷 : 𝐵 ⟶ ℝ*