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