Metamath Proof Explorer

Definition df-mdeg

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 . (Contributed by Stefan O'Rear, 19-Mar-2015) (Revised by AV, 25-Jun-2019)

Ref Expression
Assertion df-mdeg ⊢ mDeg = i ∈ V , r ∈ V ⟼ f ∈ Base i mPoly r ⟼ sup ran ⁡ h ∈ supp 0 r⁡ f ⟼ ∑ ℂ fld h ℝ * <

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmdg class mDeg
1 vi setvar i
2 cvv class V
3 vr setvar r
4 vf setvar f
5 cbs class Base
6 1 cv setvar i
7 cmpl class mPoly
8 3 cv setvar r
9 6 8 7 co class i mPoly r
10 9 5 cfv class Base i mPoly r
11 vh setvar h
12 4 cv setvar f
13 csupp class supp
14 c0g class 0 𝑔
15 8 14 cfv class 0 r
16 12 15 13 co class supp 0 r⁡ f
17 ccnfld class ℂ fld
18 cgsu class Σ𝑔
19 11 cv setvar h
20 17 19 18 co class ∑ ℂ fld h
21 11 16 20 cmpt class h ∈ supp 0 r⁡ f ⟼ ∑ ℂ fld h
22 21 crn class ran ⁡ h ∈ supp 0 r⁡ f ⟼ ∑ ℂ fld h
23 cxr class ℝ *
24 clt class <
25 22 23 24 csup class sup ran ⁡ h ∈ supp 0 r⁡ f ⟼ ∑ ℂ fld h ℝ * <
26 4 10 25 cmpt class f ∈ Base i mPoly r ⟼ sup ran ⁡ h ∈ supp 0 r⁡ f ⟼ ∑ ℂ fld h ℝ * <
27 1 3 2 2 26 cmpo class i ∈ V , r ∈ V ⟼ f ∈ Base i mPoly r ⟼ sup ran ⁡ h ∈ supp 0 r⁡ f ⟼ ∑ ℂ fld h ℝ * <
28 0 27 wceq wff mDeg = i ∈ V , r ∈ V ⟼ f ∈ Base i mPoly r ⟼ sup ran ⁡ h ∈ supp 0 r⁡ f ⟼ ∑ ℂ fld h ℝ * <