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 39637
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 39640. 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 39635 . 2 class IntgOver
2 vs . . 3 setvar 𝑠
3 cc 10523 . . . 4 class
43cpw 4535 . . 3 class 𝒫 ℂ
5 vx . . . . . . . . 9 setvar 𝑥
65cv 1527 . . . . . . . 8 class 𝑥
7 vp . . . . . . . . 9 setvar 𝑝
87cv 1527 . . . . . . . 8 class 𝑝
96, 8cfv 6348 . . . . . . 7 class (𝑝𝑥)
10 cc0 10525 . . . . . . 7 class 0
119, 10wceq 1528 . . . . . 6 wff (𝑝𝑥) = 0
12 cdgr 24704 . . . . . . . . 9 class deg
138, 12cfv 6348 . . . . . . . 8 class (deg‘𝑝)
14 ccoe 24703 . . . . . . . . 9 class coeff
158, 14cfv 6348 . . . . . . . 8 class (coeff‘𝑝)
1613, 15cfv 6348 . . . . . . 7 class ((coeff‘𝑝)‘(deg‘𝑝))
17 c1 10526 . . . . . . 7 class 1
1816, 17wceq 1528 . . . . . 6 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
1911, 18wa 396 . . . . 5 wff ((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
202cv 1527 . . . . . 6 class 𝑠
21 cply 24701 . . . . . 6 class Poly
2220, 21cfv 6348 . . . . 5 class (Poly‘𝑠)
2319, 7, 22wrex 3136 . . . 4 wff 𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
2423, 5, 3crab 3139 . . 3 class {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}
252, 4, 24cmpt 5137 . 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
261, 25wceq 1528 1 wff IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
Colors of variables: wff setvar class
This definition is referenced by:  itgoval  39639  itgocn  39642
  Copyright terms: Public domain W3C validator