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
|- D = ( deg1 ` R )
deg1z.p
|- P = ( Poly1 ` R )
deg1z.z
|- .0. = ( 0g ` P )
Assertion deg1z
|- ( R e. Ring -> ( D ` .0. ) = -oo )

Proof

Step Hyp Ref Expression
1 deg1z.d
 |-  D = ( deg1 ` R )
2 deg1z.p
 |-  P = ( Poly1 ` R )
3 deg1z.z
 |-  .0. = ( 0g ` P )
4 1on
 |-  1o e. On
5 1 deg1fval
 |-  D = ( 1o mDeg R )
6 eqid
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
7 6 2 3 ply1mpl0
 |-  .0. = ( 0g ` ( 1o mPoly R ) )
8 5 6 7 mdeg0
 |-  ( ( 1o e. On /\ R e. Ring ) -> ( D ` .0. ) = -oo )
9 4 8 mpan
 |-  ( R e. Ring -> ( D ` .0. ) = -oo )