MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mdeg Structured version   Unicode version

Definition df-mdeg 22280
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 22415. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by AV, 25-Jun-2019.)
Assertion
Ref Expression
df-mdeg  |- mDeg  =  ( i  e.  _V , 
r  e.  _V  |->  ( f  e.  ( Base `  ( i mPoly  r ) )  |->  sup ( ran  (
h  e.  ( f supp  ( 0g `  r
) )  |->  (fld  gsumg  h ) ) , 
RR* ,  <  ) ) )
Distinct variable group:    i, r, h, f

Detailed syntax breakdown of Definition df-mdeg
StepHypRef Expression
1 cmdg 22278 . 2  class mDeg
2 vi . . 3  setvar  i
3 vr . . 3  setvar  r
4 cvv 3113 . . 3  class  _V
5 vf . . . 4  setvar  f
62cv 1378 . . . . . 6  class  i
73cv 1378 . . . . . 6  class  r
8 cmpl 17813 . . . . . 6  class mPoly
96, 7, 8co 6285 . . . . 5  class  ( i mPoly 
r )
10 cbs 14493 . . . . 5  class  Base
119, 10cfv 5588 . . . 4  class  ( Base `  ( i mPoly  r ) )
12 vh . . . . . . 7  setvar  h
135cv 1378 . . . . . . . 8  class  f
14 c0g 14698 . . . . . . . . 9  class  0g
157, 14cfv 5588 . . . . . . . 8  class  ( 0g
`  r )
16 csupp 6902 . . . . . . . 8  class supp
1713, 15, 16co 6285 . . . . . . 7  class  ( f supp  ( 0g `  r
) )
18 ccnfld 18231 . . . . . . . 8  classfld
1912cv 1378 . . . . . . . 8  class  h
20 cgsu 14699 . . . . . . . 8  class  gsumg
2118, 19, 20co 6285 . . . . . . 7  class  (fld  gsumg  h )
2212, 17, 21cmpt 4505 . . . . . 6  class  ( h  e.  ( f supp  ( 0g `  r ) ) 
|->  (fld 
gsumg  h ) )
2322crn 5000 . . . . 5  class  ran  (
h  e.  ( f supp  ( 0g `  r
) )  |->  (fld  gsumg  h ) )
24 cxr 9628 . . . . 5  class  RR*
25 clt 9629 . . . . 5  class  <
2623, 24, 25csup 7901 . . . 4  class  sup ( ran  ( h  e.  ( f supp  ( 0g `  r ) )  |->  (fld  gsumg  h ) ) ,  RR* ,  <  )
275, 11, 26cmpt 4505 . . 3  class  ( f  e.  ( Base `  (
i mPoly  r ) ) 
|->  sup ( ran  (
h  e.  ( f supp  ( 0g `  r
) )  |->  (fld  gsumg  h ) ) , 
RR* ,  <  ) )
282, 3, 4, 4, 27cmpt2 6287 . 2  class  ( i  e.  _V ,  r  e.  _V  |->  ( f  e.  ( Base `  (
i mPoly  r ) ) 
|->  sup ( ran  (
h  e.  ( f supp  ( 0g `  r
) )  |->  (fld  gsumg  h ) ) , 
RR* ,  <  ) ) )
291, 28wceq 1379 1  wff mDeg  =  ( i  e.  _V , 
r  e.  _V  |->  ( f  e.  ( Base `  ( i mPoly  r ) )  |->  sup ( ran  (
h  e.  ( f supp  ( 0g `  r
) )  |->  (fld  gsumg  h ) ) , 
RR* ,  <  ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  reldmmdeg  22282  mdegfval  22287
  Copyright terms: Public domain W3C validator