This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ℎ ) ) , ℝ* , < ) ) )