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 38255
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 38258. 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 38253 . 2 class IntgOver
2 vs . . 3 setvar 𝑠
3 cc 10136 . . . 4 class
43cpw 4297 . . 3 class 𝒫 ℂ
5 vx . . . . . . . . 9 setvar 𝑥
65cv 1630 . . . . . . . 8 class 𝑥
7 vp . . . . . . . . 9 setvar 𝑝
87cv 1630 . . . . . . . 8 class 𝑝
96, 8cfv 6031 . . . . . . 7 class (𝑝𝑥)
10 cc0 10138 . . . . . . 7 class 0
119, 10wceq 1631 . . . . . 6 wff (𝑝𝑥) = 0
12 cdgr 24163 . . . . . . . . 9 class deg
138, 12cfv 6031 . . . . . . . 8 class (deg‘𝑝)
14 ccoe 24162 . . . . . . . . 9 class coeff
158, 14cfv 6031 . . . . . . . 8 class (coeff‘𝑝)
1613, 15cfv 6031 . . . . . . 7 class ((coeff‘𝑝)‘(deg‘𝑝))
17 c1 10139 . . . . . . 7 class 1
1816, 17wceq 1631 . . . . . 6 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
1911, 18wa 382 . . . . 5 wff ((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
202cv 1630 . . . . . 6 class 𝑠
21 cply 24160 . . . . . 6 class Poly
2220, 21cfv 6031 . . . . 5 class (Poly‘𝑠)
2319, 7, 22wrex 3062 . . . 4 wff 𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
2423, 5, 3crab 3065 . . 3 class {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}
252, 4, 24cmpt 4863 . 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
261, 25wceq 1631 1 wff IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
Colors of variables: wff setvar class
This definition is referenced by:  itgoval  38257  itgocn  38260
  Copyright terms: Public domain W3C validator