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

Definition df-mdeg 22557
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 22692. (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 22555 . 2  class mDeg
2 vi . . 3  setvar  i
3 vr . . 3  setvar  r
4 cvv 3047 . . 3  class  _V
5 vf . . . 4  setvar  f
62cv 1398 . . . . . 6  class  i
73cv 1398 . . . . . 6  class  r
8 cmpl 18134 . . . . . 6  class mPoly
96, 7, 8co 6214 . . . . 5  class  ( i mPoly 
r )
10 cbs 14653 . . . . 5  class  Base
119, 10cfv 5509 . . . 4  class  ( Base `  ( i mPoly  r ) )
12 vh . . . . . . 7  setvar  h
135cv 1398 . . . . . . . 8  class  f
14 c0g 14866 . . . . . . . . 9  class  0g
157, 14cfv 5509 . . . . . . . 8  class  ( 0g
`  r )
16 csupp 6835 . . . . . . . 8  class supp
1713, 15, 16co 6214 . . . . . . 7  class  ( f supp  ( 0g `  r
) )
18 ccnfld 18552 . . . . . . . 8  classfld
1912cv 1398 . . . . . . . 8  class  h
20 cgsu 14867 . . . . . . . 8  class  gsumg
2118, 19, 20co 6214 . . . . . . 7  class  (fld  gsumg  h )
2212, 17, 21cmpt 4438 . . . . . 6  class  ( h  e.  ( f supp  ( 0g `  r ) ) 
|->  (fld 
gsumg  h ) )
2322crn 4927 . . . . 5  class  ran  (
h  e.  ( f supp  ( 0g `  r
) )  |->  (fld  gsumg  h ) )
24 cxr 9556 . . . . 5  class  RR*
25 clt 9557 . . . . 5  class  <
2623, 24, 25csup 7833 . . . 4  class  sup ( ran  ( h  e.  ( f supp  ( 0g `  r ) )  |->  (fld  gsumg  h ) ) ,  RR* ,  <  )
275, 11, 26cmpt 4438 . . 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 6216 . 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 1399 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  22559  mdegfval  22564
  Copyright terms: Public domain W3C validator