Detailed syntax breakdown of Definition df-mdeg
Step | Hyp | Ref
| Expression |
1 | | cmdg 24815 |
. 2
class
mDeg |
2 | | vi |
. . 3
setvar 𝑖 |
3 | | vr |
. . 3
setvar 𝑟 |
4 | | cvv 3400 |
. . 3
class
V |
5 | | vf |
. . . 4
setvar 𝑓 |
6 | 2 | cv 1541 |
. . . . . 6
class 𝑖 |
7 | 3 | cv 1541 |
. . . . . 6
class 𝑟 |
8 | | cmpl 20731 |
. . . . . 6
class
mPoly |
9 | 6, 7, 8 | co 7182 |
. . . . 5
class (𝑖 mPoly 𝑟) |
10 | | cbs 16598 |
. . . . 5
class
Base |
11 | 9, 10 | cfv 6349 |
. . . 4
class
(Base‘(𝑖 mPoly
𝑟)) |
12 | | vh |
. . . . . . 7
setvar ℎ |
13 | 5 | cv 1541 |
. . . . . . . 8
class 𝑓 |
14 | | c0g 16828 |
. . . . . . . . 9
class
0g |
15 | 7, 14 | cfv 6349 |
. . . . . . . 8
class
(0g‘𝑟) |
16 | | csupp 7868 |
. . . . . . . 8
class
supp |
17 | 13, 15, 16 | co 7182 |
. . . . . . 7
class (𝑓 supp (0g‘𝑟)) |
18 | | ccnfld 20229 |
. . . . . . . 8
class
ℂfld |
19 | 12 | cv 1541 |
. . . . . . . 8
class ℎ |
20 | | cgsu 16829 |
. . . . . . . 8
class
Σg |
21 | 18, 19, 20 | co 7182 |
. . . . . . 7
class
(ℂfld Σg ℎ) |
22 | 12, 17, 21 | cmpt 5120 |
. . . . . 6
class (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld
Σg ℎ)) |
23 | 22 | crn 5536 |
. . . . 5
class ran
(ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦
(ℂfld Σg ℎ)) |
24 | | cxr 10764 |
. . . . 5
class
ℝ* |
25 | | clt 10765 |
. . . . 5
class
< |
26 | 23, 24, 25 | csup 8989 |
. . . 4
class sup(ran
(ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦
(ℂfld Σg ℎ)), ℝ*, <
) |
27 | 5, 11, 26 | cmpt 5120 |
. . 3
class (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ sup(ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld
Σg ℎ)), ℝ*, <
)) |
28 | 2, 3, 4, 4, 27 | cmpo 7184 |
. 2
class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ sup(ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld
Σg ℎ)), ℝ*, <
))) |
29 | 1, 28 | wceq 1542 |
1
wff mDeg =
(𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ sup(ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld
Σg ℎ)), ℝ*, <
))) |