Detailed syntax breakdown of Definition df-mdeg
Step | Hyp | Ref
| Expression |
1 | | cmdg 25224 |
. 2
class
mDeg |
2 | | vi |
. . 3
setvar 𝑖 |
3 | | vr |
. . 3
setvar 𝑟 |
4 | | cvv 3433 |
. . 3
class
V |
5 | | vf |
. . . 4
setvar 𝑓 |
6 | 2 | cv 1538 |
. . . . . 6
class 𝑖 |
7 | 3 | cv 1538 |
. . . . . 6
class 𝑟 |
8 | | cmpl 21118 |
. . . . . 6
class
mPoly |
9 | 6, 7, 8 | co 7284 |
. . . . 5
class (𝑖 mPoly 𝑟) |
10 | | cbs 16921 |
. . . . 5
class
Base |
11 | 9, 10 | cfv 6437 |
. . . 4
class
(Base‘(𝑖 mPoly
𝑟)) |
12 | | vh |
. . . . . . 7
setvar ℎ |
13 | 5 | cv 1538 |
. . . . . . . 8
class 𝑓 |
14 | | c0g 17159 |
. . . . . . . . 9
class
0g |
15 | 7, 14 | cfv 6437 |
. . . . . . . 8
class
(0g‘𝑟) |
16 | | csupp 7986 |
. . . . . . . 8
class
supp |
17 | 13, 15, 16 | co 7284 |
. . . . . . 7
class (𝑓 supp (0g‘𝑟)) |
18 | | ccnfld 20606 |
. . . . . . . 8
class
ℂfld |
19 | 12 | cv 1538 |
. . . . . . . 8
class ℎ |
20 | | cgsu 17160 |
. . . . . . . 8
class
Σg |
21 | 18, 19, 20 | co 7284 |
. . . . . . 7
class
(ℂfld Σg ℎ) |
22 | 12, 17, 21 | cmpt 5158 |
. . . . . 6
class (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld
Σg ℎ)) |
23 | 22 | crn 5591 |
. . . . 5
class ran
(ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦
(ℂfld Σg ℎ)) |
24 | | cxr 11017 |
. . . . 5
class
ℝ* |
25 | | clt 11018 |
. . . . 5
class
< |
26 | 23, 24, 25 | csup 9208 |
. . . 4
class sup(ran
(ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦
(ℂfld Σg ℎ)), ℝ*, <
) |
27 | 5, 11, 26 | cmpt 5158 |
. . 3
class (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ sup(ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld
Σg ℎ)), ℝ*, <
)) |
28 | 2, 3, 4, 4, 27 | cmpo 7286 |
. 2
class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ sup(ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld
Σg ℎ)), ℝ*, <
))) |
29 | 1, 28 | wceq 1539 |
1
wff mDeg =
(𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ sup(ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld
Σg ℎ)), ℝ*, <
))) |