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

Definition df-mdeg 21483
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 21618. (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 21481 . 2  class mDeg
2 vi . . 3  setvar  i
3 vr . . 3  setvar  r
4 cvv 2970 . . 3  class  _V
5 vf . . . 4  setvar  f
62cv 1363 . . . . . 6  class  i
73cv 1363 . . . . . 6  class  r
8 cmpl 17398 . . . . . 6  class mPoly
96, 7, 8co 6090 . . . . 5  class  ( i mPoly 
r )
10 cbs 14170 . . . . 5  class  Base
119, 10cfv 5415 . . . 4  class  ( Base `  ( i mPoly  r ) )
12 vh . . . . . . 7  setvar  h
135cv 1363 . . . . . . . 8  class  f
14 c0g 14374 . . . . . . . . 9  class  0g
157, 14cfv 5415 . . . . . . . 8  class  ( 0g
`  r )
16 csupp 6689 . . . . . . . 8  class supp
1713, 15, 16co 6090 . . . . . . 7  class  ( f supp  ( 0g `  r
) )
18 ccnfld 17777 . . . . . . . 8  classfld
1912cv 1363 . . . . . . . 8  class  h
20 cgsu 14375 . . . . . . . 8  class  gsumg
2118, 19, 20co 6090 . . . . . . 7  class  (fld  gsumg  h )
2212, 17, 21cmpt 4347 . . . . . 6  class  ( h  e.  ( f supp  ( 0g `  r ) ) 
|->  (fld 
gsumg  h ) )
2322crn 4837 . . . . 5  class  ran  (
h  e.  ( f supp  ( 0g `  r
) )  |->  (fld  gsumg  h ) )
24 cxr 9413 . . . . 5  class  RR*
25 clt 9414 . . . . 5  class  <
2623, 24, 25csup 7686 . . . 4  class  sup ( ran  ( h  e.  ( f supp  ( 0g `  r ) )  |->  (fld  gsumg  h ) ) ,  RR* ,  <  )
275, 11, 26cmpt 4347 . . 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 6092 . 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 1364 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  21485  mdegfval  21490
  Copyright terms: Public domain W3C validator