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 = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ sup ( ran ( ∈ ( 𝑓 supp ( 0g𝑟 ) ) ↦ ( ℂfld Σg ) ) , ℝ* , < ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmdg mDeg
1 vi 𝑖
2 cvv V
3 vr 𝑟
4 vf 𝑓
5 cbs Base
6 1 cv 𝑖
7 cmpl mPoly
8 3 cv 𝑟
9 6 8 7 co ( 𝑖 mPoly 𝑟 )
10 9 5 cfv ( Base ‘ ( 𝑖 mPoly 𝑟 ) )
11 vh
12 4 cv 𝑓
13 csupp supp
14 c0g 0g
15 8 14 cfv ( 0g𝑟 )
16 12 15 13 co ( 𝑓 supp ( 0g𝑟 ) )
17 ccnfld fld
18 cgsu Σg
19 11 cv
20 17 19 18 co ( ℂfld Σg )
21 11 16 20 cmpt ( ∈ ( 𝑓 supp ( 0g𝑟 ) ) ↦ ( ℂfld Σg ) )
22 21 crn ran ( ∈ ( 𝑓 supp ( 0g𝑟 ) ) ↦ ( ℂfld Σg ) )
23 cxr *
24 clt <
25 22 23 24 csup sup ( ran ( ∈ ( 𝑓 supp ( 0g𝑟 ) ) ↦ ( ℂfld Σg ) ) , ℝ* , < )
26 4 10 25 cmpt ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ sup ( ran ( ∈ ( 𝑓 supp ( 0g𝑟 ) ) ↦ ( ℂfld Σg ) ) , ℝ* , < ) )
27 1 3 2 2 26 cmpo ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ sup ( ran ( ∈ ( 𝑓 supp ( 0g𝑟 ) ) ↦ ( ℂfld Σg ) ) , ℝ* , < ) ) )
28 0 27 wceq mDeg = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ sup ( ran ( ∈ ( 𝑓 supp ( 0g𝑟 ) ) ↦ ( ℂfld Σg ) ) , ℝ* , < ) ) )