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 42725
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 42728. 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 42723 . 2 class IntgOver
2 vs . . 3 setvar 𝑠
3 cc 11138 . . . 4 class
43cpw 4604 . . 3 class 𝒫 ℂ
5 vx . . . . . . . . 9 setvar 𝑥
65cv 1532 . . . . . . . 8 class 𝑥
7 vp . . . . . . . . 9 setvar 𝑝
87cv 1532 . . . . . . . 8 class 𝑝
96, 8cfv 6549 . . . . . . 7 class (𝑝𝑥)
10 cc0 11140 . . . . . . 7 class 0
119, 10wceq 1533 . . . . . 6 wff (𝑝𝑥) = 0
12 cdgr 26166 . . . . . . . . 9 class deg
138, 12cfv 6549 . . . . . . . 8 class (deg‘𝑝)
14 ccoe 26165 . . . . . . . . 9 class coeff
158, 14cfv 6549 . . . . . . . 8 class (coeff‘𝑝)
1613, 15cfv 6549 . . . . . . 7 class ((coeff‘𝑝)‘(deg‘𝑝))
17 c1 11141 . . . . . . 7 class 1
1816, 17wceq 1533 . . . . . 6 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
1911, 18wa 394 . . . . 5 wff ((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
202cv 1532 . . . . . 6 class 𝑠
21 cply 26163 . . . . . 6 class Poly
2220, 21cfv 6549 . . . . 5 class (Poly‘𝑠)
2319, 7, 22wrex 3059 . . . 4 wff 𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
2423, 5, 3crab 3418 . . 3 class {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}
252, 4, 24cmpt 5232 . 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
261, 25wceq 1533 1 wff IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
Colors of variables: wff setvar class
This definition is referenced by:  itgoval  42727  itgocn  42730
  Copyright terms: Public domain W3C validator