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