Metamath Proof Explorer

Definition df-deg1

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

Ref Expression
Assertion df-deg1 
|- deg1 = ( r e. _V |-> ( 1o mDeg r ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdg1 
 |-  deg1
1 vr 
 |-  r
2 cvv 
 |-  _V
3 c1o 
 |-  1o
4 cmdg 
 |-  mDeg
5 1 cv 
 |-  r
6 3 5 4 co 
 |-  ( 1o mDeg r )
7 1 2 6 cmpt 
 |-  ( r e. _V |-> ( 1o mDeg r ) )
8 0 7 wceq 
 |-  deg1 = ( r e. _V |-> ( 1o mDeg r ) )