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

Definition df-mdeg 19457
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 19589. (Contributed by Stefan O'Rear, 19-Mar-2015.)
Assertion
Ref Expression
df-mdeg  |- mDeg  =  ( i  e.  _V , 
r  e.  _V  |->  ( f  e.  ( Base `  ( i mPoly  r ) )  |->  sup ( ran  (
h  e.  ( `' f " ( _V 
\  { ( 0g
`  r ) } ) )  |->  (fld  gsumg  h ) ) , 
RR* ,  <  ) ) )
Distinct variable group:    i, r, h, f

Detailed syntax breakdown of Definition df-mdeg
StepHypRef Expression
1 cmdg 19455 . 2  class mDeg
2 vi . . 3  set  i
3 vr . . 3  set  r
4 cvv 2801 . . 3  class  _V
5 vf . . . 4  set  f
62cv 1631 . . . . . 6  class  i
73cv 1631 . . . . . 6  class  r
8 cmpl 16105 . . . . . 6  class mPoly
96, 7, 8co 5874 . . . . 5  class  ( i mPoly 
r )
10 cbs 13164 . . . . 5  class  Base
119, 10cfv 5271 . . . 4  class  ( Base `  ( i mPoly  r ) )
12 vh . . . . . . 7  set  h
135cv 1631 . . . . . . . . 9  class  f
1413ccnv 4704 . . . . . . . 8  class  `' f
15 c0g 13416 . . . . . . . . . . 11  class  0g
167, 15cfv 5271 . . . . . . . . . 10  class  ( 0g
`  r )
1716csn 3653 . . . . . . . . 9  class  { ( 0g `  r ) }
184, 17cdif 3162 . . . . . . . 8  class  ( _V 
\  { ( 0g
`  r ) } )
1914, 18cima 4708 . . . . . . 7  class  ( `' f " ( _V 
\  { ( 0g
`  r ) } ) )
20 ccnfld 16393 . . . . . . . 8  classfld
2112cv 1631 . . . . . . . 8  class  h
22 cgsu 13417 . . . . . . . 8  class  gsumg
2320, 21, 22co 5874 . . . . . . 7  class  (fld  gsumg  h )
2412, 19, 23cmpt 4093 . . . . . 6  class  ( h  e.  ( `' f
" ( _V  \  { ( 0g `  r ) } ) )  |->  (fld 
gsumg  h ) )
2524crn 4706 . . . . 5  class  ran  (
h  e.  ( `' f " ( _V 
\  { ( 0g
`  r ) } ) )  |->  (fld  gsumg  h ) )
26 cxr 8882 . . . . 5  class  RR*
27 clt 8883 . . . . 5  class  <
2825, 26, 27csup 7209 . . . 4  class  sup ( ran  ( h  e.  ( `' f " ( _V  \  { ( 0g
`  r ) } ) )  |->  (fld  gsumg  h ) ) , 
RR* ,  <  )
295, 11, 28cmpt 4093 . . 3  class  ( f  e.  ( Base `  (
i mPoly  r ) ) 
|->  sup ( ran  (
h  e.  ( `' f " ( _V 
\  { ( 0g
`  r ) } ) )  |->  (fld  gsumg  h ) ) , 
RR* ,  <  ) )
302, 3, 4, 4, 29cmpt2 5876 . 2  class  ( i  e.  _V ,  r  e.  _V  |->  ( f  e.  ( Base `  (
i mPoly  r ) ) 
|->  sup ( ran  (
h  e.  ( `' f " ( _V 
\  { ( 0g
`  r ) } ) )  |->  (fld  gsumg  h ) ) , 
RR* ,  <  ) ) )
311, 30wceq 1632 1  wff mDeg  =  ( i  e.  _V , 
r  e.  _V  |->  ( f  e.  ( Base `  ( i mPoly  r ) )  |->  sup ( ran  (
h  e.  ( `' f " ( _V 
\  { ( 0g
`  r ) } ) )  |->  (fld  gsumg  h ) ) , 
RR* ,  <  ) ) )
Colors of variables: wff set class
This definition is referenced by:  reldmmdeg  19459  mdegfval  19464
  Copyright terms: Public domain W3C validator