Metamath Proof Explorer


Theorem deg1cl

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

Ref Expression
Hypotheses deg1xrf.d 𝐷 = ( deg1𝑅 )
deg1xrf.p 𝑃 = ( Poly1𝑅 )
deg1xrf.b 𝐵 = ( Base ‘ 𝑃 )
Assertion deg1cl ( 𝐹𝐵 → ( 𝐷𝐹 ) ∈ ( ℕ0 ∪ { -∞ } ) )

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 mdegcl ( 𝐹𝐵 → ( 𝐷𝐹 ) ∈ ( ℕ0 ∪ { -∞ } ) )