Detailed syntax breakdown of Definition df-itgo
| Step | Hyp | Ref
| Expression |
| 1 | | citgo 43147 |
. 2
class
IntgOver |
| 2 | | vs |
. . 3
setvar 𝑠 |
| 3 | | cc 11149 |
. . . 4
class
ℂ |
| 4 | 3 | cpw 4598 |
. . 3
class 𝒫
ℂ |
| 5 | | vx |
. . . . . . . . 9
setvar 𝑥 |
| 6 | 5 | cv 1539 |
. . . . . . . 8
class 𝑥 |
| 7 | | vp |
. . . . . . . . 9
setvar 𝑝 |
| 8 | 7 | cv 1539 |
. . . . . . . 8
class 𝑝 |
| 9 | 6, 8 | cfv 6559 |
. . . . . . 7
class (𝑝‘𝑥) |
| 10 | | cc0 11151 |
. . . . . . 7
class
0 |
| 11 | 9, 10 | wceq 1540 |
. . . . . 6
wff (𝑝‘𝑥) = 0 |
| 12 | | cdgr 26216 |
. . . . . . . . 9
class
deg |
| 13 | 8, 12 | cfv 6559 |
. . . . . . . 8
class
(deg‘𝑝) |
| 14 | | ccoe 26215 |
. . . . . . . . 9
class
coeff |
| 15 | 8, 14 | cfv 6559 |
. . . . . . . 8
class
(coeff‘𝑝) |
| 16 | 13, 15 | cfv 6559 |
. . . . . . 7
class
((coeff‘𝑝)‘(deg‘𝑝)) |
| 17 | | c1 11152 |
. . . . . . 7
class
1 |
| 18 | 16, 17 | wceq 1540 |
. . . . . 6
wff
((coeff‘𝑝)‘(deg‘𝑝)) = 1 |
| 19 | 11, 18 | wa 395 |
. . . . 5
wff ((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1) |
| 20 | 2 | cv 1539 |
. . . . . 6
class 𝑠 |
| 21 | | cply 26213 |
. . . . . 6
class
Poly |
| 22 | 20, 21 | cfv 6559 |
. . . . 5
class
(Poly‘𝑠) |
| 23 | 19, 7, 22 | wrex 3069 |
. . . 4
wff
∃𝑝 ∈
(Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1) |
| 24 | 23, 5, 3 | crab 3435 |
. . 3
class {𝑥 ∈ ℂ ∣
∃𝑝 ∈
(Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)} |
| 25 | 2, 4, 24 | cmpt 5223 |
. 2
class (𝑠 ∈ 𝒫 ℂ
↦ {𝑥 ∈ ℂ
∣ ∃𝑝 ∈
(Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}) |
| 26 | 1, 25 | wceq 1540 |
1
wff IntgOver =
(𝑠 ∈ 𝒫 ℂ
↦ {𝑥 ∈ ℂ
∣ ∃𝑝 ∈
(Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}) |