Metamath Proof Explorer

Definition df-mdeg

Description: Define the degree of a polynomial. Note (SO): as an experiment I am using a definition which makes the degree of the zero polynomial -oo , contrary to the convention used in df-dgr . (Contributed by Stefan O'Rear, 19-Mar-2015) (Revised by AV, 25-Jun-2019)

Ref Expression
Assertion df-mdeg 
|- mDeg = ( i e. _V , r e. _V |-> ( f e. ( Base ` ( i mPoly r ) ) |-> sup ( ran ( h e. ( f supp ( 0g ` r ) ) |-> ( CCfld gsum h ) ) , RR* , < ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmdg 
 |-  mDeg
1 vi 
 |-  i
2 cvv 
 |-  _V
3 vr 
 |-  r
4 vf 
 |-  f
5 cbs 
 |-  Base
6 1 cv 
 |-  i
7 cmpl 
 |-  mPoly
8 3 cv 
 |-  r
9 6 8 7 co 
 |-  ( i mPoly r )
10 9 5 cfv 
 |-  ( Base ` ( i mPoly r ) )
11 vh 
 |-  h
12 4 cv 
 |-  f
13 csupp 
 |-  supp
14 c0g 
 |-  0g
15 8 14 cfv 
 |-  ( 0g ` r )
16 12 15 13 co 
 |-  ( f supp ( 0g ` r ) )
17 ccnfld 
 |-  CCfld
18 cgsu 
 |-  gsum
19 11 cv 
 |-  h
20 17 19 18 co 
 |-  ( CCfld gsum h )
21 11 16 20 cmpt 
 |-  ( h e. ( f supp ( 0g ` r ) ) |-> ( CCfld gsum h ) )
22 21 crn 
 |-  ran ( h e. ( f supp ( 0g ` r ) ) |-> ( CCfld gsum h ) )
23 cxr 
 |-  RR*
24 clt 
 |-  <
25 22 23 24 csup 
 |-  sup ( ran ( h e. ( f supp ( 0g ` r ) ) |-> ( CCfld gsum h ) ) , RR* , < )
26 4 10 25 cmpt 
 |-  ( f e. ( Base ` ( i mPoly r ) ) |-> sup ( ran ( h e. ( f supp ( 0g ` r ) ) |-> ( CCfld gsum h ) ) , RR* , < ) )
27 1 3 2 2 26 cmpo 
 |-  ( i e. _V , r e. _V |-> ( f e. ( Base ` ( i mPoly r ) ) |-> sup ( ran ( h e. ( f supp ( 0g ` r ) ) |-> ( CCfld gsum h ) ) , RR* , < ) ) )
28 0 27 wceq 
 |-  mDeg = ( i e. _V , r e. _V |-> ( f e. ( Base ` ( i mPoly r ) ) |-> sup ( ran ( h e. ( f supp ( 0g ` r ) ) |-> ( CCfld gsum h ) ) , RR* , < ) ) )