Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-itgo Structured version   Visualization version   GIF version

Definition df-itgo 39265
Description: A complex number is said to be integral over a subset if it is the root of a monic polynomial with coefficients from the subset. This definition is typically not used for fields but it works there, see aaitgo 39268. This definition could work for subsets of an arbitrary ring with a more general definition of polynomials. TODO: use Monic. (Contributed by Stefan O'Rear, 27-Nov-2014.)
Assertion
Ref Expression
df-itgo IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
Distinct variable group:   𝑥,𝑝,𝑠

Detailed syntax breakdown of Definition df-itgo
StepHypRef Expression
1 citgo 39263 . 2 class IntgOver
2 vs . . 3 setvar 𝑠
3 cc 10388 . . . 4 class
43cpw 4459 . . 3 class 𝒫 ℂ
5 vx . . . . . . . . 9 setvar 𝑥
65cv 1524 . . . . . . . 8 class 𝑥
7 vp . . . . . . . . 9 setvar 𝑝
87cv 1524 . . . . . . . 8 class 𝑝
96, 8cfv 6232 . . . . . . 7 class (𝑝𝑥)
10 cc0 10390 . . . . . . 7 class 0
119, 10wceq 1525 . . . . . 6 wff (𝑝𝑥) = 0
12 cdgr 24464 . . . . . . . . 9 class deg
138, 12cfv 6232 . . . . . . . 8 class (deg‘𝑝)
14 ccoe 24463 . . . . . . . . 9 class coeff
158, 14cfv 6232 . . . . . . . 8 class (coeff‘𝑝)
1613, 15cfv 6232 . . . . . . 7 class ((coeff‘𝑝)‘(deg‘𝑝))
17 c1 10391 . . . . . . 7 class 1
1816, 17wceq 1525 . . . . . 6 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
1911, 18wa 396 . . . . 5 wff ((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
202cv 1524 . . . . . 6 class 𝑠
21 cply 24461 . . . . . 6 class Poly
2220, 21cfv 6232 . . . . 5 class (Poly‘𝑠)
2319, 7, 22wrex 3108 . . . 4 wff 𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
2423, 5, 3crab 3111 . . 3 class {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}
252, 4, 24cmpt 5047 . 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
261, 25wceq 1525 1 wff IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
Colors of variables: wff setvar class
This definition is referenced by:  itgoval  39267  itgocn  39270
  Copyright terms: Public domain W3C validator