Definition df-mdeg 23815

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 23947. (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

Step	Hyp	Ref	Expression
1		cmdg 23813	. 2 class mDeg
2		vi	. . 3 setvar i
3		vr	. . 3 setvar r
4		cvv 3200	. . 3 class _V
5		vf	. . . 4 setvar f
6	2	cv 1482	. . . . . 6 class i
7	3	cv 1482	. . . . . 6 class r
8		cmpl 19353	. . . . . 6 class mPoly
9	6, 7, 8	co 6650	. . . . 5 class ( i mPoly r )
10		cbs 15857	. . . . 5 class Base
11	9, 10	cfv 5888	. . . 4 class ( Base ` ( i mPoly r ) )
12		vh	. . . . . . 7 setvar h
13	5	cv 1482	. . . . . . . 8 class f
14		c0g 16100	. . . . . . . . 9 class 0g
15	7, 14	cfv 5888	. . . . . . . 8 class ( 0g ` r )
16		csupp 7295	. . . . . . . 8 class supp
17	13, 15, 16	co 6650	. . . . . . 7 class ( f supp ( 0g ` r ) )
18		ccnfld 19746	. . . . . . . 8 class ℂfld
19	12	cv 1482	. . . . . . . 8 class h
20		cgsu 16101	. . . . . . . 8 class gsumg
21	18, 19, 20	co 6650	. . . . . . 7 class (ℂfld gsumg h )
22	12, 17, 21	cmpt 4729	. . . . . 6 class ( h e. ( f supp ( 0g ` r ) ) |-> (ℂfld gsumg h ) )
23	22	crn 5115	. . . . 5 class ran ( h e. ( f supp ( 0g ` r ) ) |-> (ℂfld gsumg h ) )
24		cxr 10073	. . . . 5 class RR*
25		clt 10074	. . . . 5 class <
26	23, 24, 25	csup 8346	. . . 4 class sup ( ran ( h e. ( f supp ( 0g ` r ) ) |-> (ℂfld gsumg h ) ) , RR* , < )
27	5, 11, 26	cmpt 4729	. . 3 class ( f e. ( Base ` ( i mPoly r ) ) |-> sup ( ran ( h e. ( f supp ( 0g ` r ) ) |-> (ℂfld gsumg h ) ) , RR* , < ) )
28	2, 3, 4, 4, 27	cmpt2 6652	. 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* , < ) ) )
29	1, 28	wceq 1483	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* , < ) ) )

This definition is referenced by:  reldmmdeg  23817  mdegfval  23822