Metamath Proof Explorer


Theorem deg1z

Description: Degree of the zero univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses deg1z.d 𝐷 = ( deg1𝑅 )
deg1z.p 𝑃 = ( Poly1𝑅 )
deg1z.z 0 = ( 0g𝑃 )
Assertion deg1z ( 𝑅 ∈ Ring → ( 𝐷0 ) = -∞ )

Proof

Step Hyp Ref Expression
1 deg1z.d 𝐷 = ( deg1𝑅 )
2 deg1z.p 𝑃 = ( Poly1𝑅 )
3 deg1z.z 0 = ( 0g𝑃 )
4 1on 1o ∈ On
5 1 deg1fval 𝐷 = ( 1o mDeg 𝑅 )
6 eqid ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
7 6 2 3 ply1mpl0 0 = ( 0g ‘ ( 1o mPoly 𝑅 ) )
8 5 6 7 mdeg0 ( ( 1o ∈ On ∧ 𝑅 ∈ Ring ) → ( 𝐷0 ) = -∞ )
9 4 8 mpan ( 𝑅 ∈ Ring → ( 𝐷0 ) = -∞ )