Definition df-mdeg 23619

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 -∞, contrary to the convention used in df-dgr 23751. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by AV, 25-Jun-2019.)

Assertion

Ref	Expression
df-mdeg	⊢ mDeg = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ sup(ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld Σg ℎ)), ℝ*, < )))

Distinct variable group:   𝑖,𝑟,ℎ,𝑓

Detailed syntax breakdown of Definition df-mdeg

Step	Hyp	Ref	Expression
1		cmdg 23617	. 2 class mDeg
2		vi	. . 3 setvar 𝑖
3		vr	. . 3 setvar 𝑟
4		cvv 3173	. . 3 class V
5		vf	. . . 4 setvar 𝑓
6	2	cv 1474	. . . . . 6 class 𝑖
7	3	cv 1474	. . . . . 6 class 𝑟
8		cmpl 19174	. . . . . 6 class mPoly
9	6, 7, 8	co 6549	. . . . 5 class (𝑖 mPoly 𝑟)
10		cbs 15695	. . . . 5 class Base
11	9, 10	cfv 5804	. . . 4 class (Base‘(𝑖 mPoly 𝑟))
12		vh	. . . . . . 7 setvar ℎ
13	5	cv 1474	. . . . . . . 8 class 𝑓
14		c0g 15923	. . . . . . . . 9 class 0g
15	7, 14	cfv 5804	. . . . . . . 8 class (0g‘𝑟)
16		csupp 7182	. . . . . . . 8 class supp
17	13, 15, 16	co 6549	. . . . . . 7 class (𝑓 supp (0g‘𝑟))
18		ccnfld 19567	. . . . . . . 8 class ℂfld
19	12	cv 1474	. . . . . . . 8 class ℎ
20		cgsu 15924	. . . . . . . 8 class Σg
21	18, 19, 20	co 6549	. . . . . . 7 class (ℂfld Σg ℎ)
22	12, 17, 21	cmpt 4643	. . . . . 6 class (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld Σg ℎ))
23	22	crn 5039	. . . . 5 class ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld Σg ℎ))
24		cxr 9952	. . . . 5 class ℝ*
25		clt 9953	. . . . 5 class <
26	23, 24, 25	csup 8229	. . . 4 class sup(ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld Σg ℎ)), ℝ*, < )
27	5, 11, 26	cmpt 4643	. . 3 class (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ sup(ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld Σg ℎ)), ℝ*, < ))
28	2, 3, 4, 4, 27	cmpt2 6551	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ sup(ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld Σg ℎ)), ℝ*, < )))
29	1, 28	wceq 1475	1 wff mDeg = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ sup(ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld Σg ℎ)), ℝ*, < )))

This definition is referenced by:  reldmmdeg  23621  mdegfval  23626