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 \in V, r \in V ⟼ (f \in {Base}_{(i mPoly r)} ⟼ sup (ran (h \in {supp}_{0_{r}} (f) ⟼ \sum_{ℂ_{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 (\sum_{ℂ_{fld}}, h)$
21	11 16 20	cmpt	$class (h \in {supp}_{0_{r}} (f) ⟼ \sum_{ℂ_{fld}} h)$
22	21	crn	$class ran (h \in {supp}_{0_{r}} (f) ⟼ \sum_{ℂ_{fld}} h)$
23		cxr	$class ℝ^{*}$
24		clt	$class <$
25	22 23 24	csup	$class sup (ran (h \in {supp}_{0_{r}} (f) ⟼ \sum_{ℂ_{fld}} h) ℝ^{*} <)$
26	4 10 25	cmpt	$class (f \in {Base}_{(i mPoly r)} ⟼ sup (ran (h \in {supp}_{0_{r}} (f) ⟼ \sum_{ℂ_{fld}} h) ℝ^{*} <))$
27	1 3 2 2 26	cmpo	$class (i \in V, r \in V ⟼ (f \in {Base}_{(i mPoly r)} ⟼ sup (ran (h \in {supp}_{0_{r}} (f) ⟼ \sum_{ℂ_{fld}} h) ℝ^{*} <)))$
28	0 27	wceq	$wff mDeg = (i \in V, r \in V ⟼ (f \in {Base}_{(i mPoly r)} ⟼ sup (ran (h \in {supp}_{0_{r}} (f) ⟼ \sum_{ℂ_{fld}} h) ℝ^{*} <)))$

Metamath Proof Explorer

Definition df-mdeg

Detailed syntax breakdown