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

Definition df-mdeg 23860
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 23992. (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
StepHypRef Expression
1 cmdg 23858 . 2 class mDeg
2 vi . . 3 setvar 𝑖
3 vr . . 3 setvar 𝑟
4 cvv 3231 . . 3 class V
5 vf . . . 4 setvar 𝑓
62cv 1522 . . . . . 6 class 𝑖
73cv 1522 . . . . . 6 class 𝑟
8 cmpl 19401 . . . . . 6 class mPoly
96, 7, 8co 6690 . . . . 5 class (𝑖 mPoly 𝑟)
10 cbs 15904 . . . . 5 class Base
119, 10cfv 5926 . . . 4 class (Base‘(𝑖 mPoly 𝑟))
12 vh . . . . . . 7 setvar
135cv 1522 . . . . . . . 8 class 𝑓
14 c0g 16147 . . . . . . . . 9 class 0g
157, 14cfv 5926 . . . . . . . 8 class (0g𝑟)
16 csupp 7340 . . . . . . . 8 class supp
1713, 15, 16co 6690 . . . . . . 7 class (𝑓 supp (0g𝑟))
18 ccnfld 19794 . . . . . . . 8 class fld
1912cv 1522 . . . . . . . 8 class
20 cgsu 16148 . . . . . . . 8 class Σg
2118, 19, 20co 6690 . . . . . . 7 class (ℂfld Σg )
2212, 17, 21cmpt 4762 . . . . . 6 class ( ∈ (𝑓 supp (0g𝑟)) ↦ (ℂfld Σg ))
2322crn 5144 . . . . 5 class ran ( ∈ (𝑓 supp (0g𝑟)) ↦ (ℂfld Σg ))
24 cxr 10111 . . . . 5 class *
25 clt 10112 . . . . 5 class <
2623, 24, 25csup 8387 . . . 4 class sup(ran ( ∈ (𝑓 supp (0g𝑟)) ↦ (ℂfld Σg )), ℝ*, < )
275, 11, 26cmpt 4762 . . 3 class (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ sup(ran ( ∈ (𝑓 supp (0g𝑟)) ↦ (ℂfld Σg )), ℝ*, < ))
282, 3, 4, 4, 27cmpt2 6692 . 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ sup(ran ( ∈ (𝑓 supp (0g𝑟)) ↦ (ℂfld Σg )), ℝ*, < )))
291, 28wceq 1523 1 wff mDeg = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ sup(ran ( ∈ (𝑓 supp (0g𝑟)) ↦ (ℂfld Σg )), ℝ*, < )))
Colors of variables: wff setvar class
This definition is referenced by:  reldmmdeg  23862  mdegfval  23867
  Copyright terms: Public domain W3C validator