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 36531
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 36534. 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 36529 . 2 class IntgOver
2 vs . . 3 setvar 𝑠
3 cc 9790 . . . 4 class
43cpw 4107 . . 3 class 𝒫 ℂ
5 vx . . . . . . . . 9 setvar 𝑥
65cv 1473 . . . . . . . 8 class 𝑥
7 vp . . . . . . . . 9 setvar 𝑝
87cv 1473 . . . . . . . 8 class 𝑝
96, 8cfv 5789 . . . . . . 7 class (𝑝𝑥)
10 cc0 9792 . . . . . . 7 class 0
119, 10wceq 1474 . . . . . 6 wff (𝑝𝑥) = 0
12 cdgr 23691 . . . . . . . . 9 class deg
138, 12cfv 5789 . . . . . . . 8 class (deg‘𝑝)
14 ccoe 23690 . . . . . . . . 9 class coeff
158, 14cfv 5789 . . . . . . . 8 class (coeff‘𝑝)
1613, 15cfv 5789 . . . . . . 7 class ((coeff‘𝑝)‘(deg‘𝑝))
17 c1 9793 . . . . . . 7 class 1
1816, 17wceq 1474 . . . . . 6 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
1911, 18wa 382 . . . . 5 wff ((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
202cv 1473 . . . . . 6 class 𝑠
21 cply 23688 . . . . . 6 class Poly
2220, 21cfv 5789 . . . . 5 class (Poly‘𝑠)
2319, 7, 22wrex 2896 . . . 4 wff 𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
2423, 5, 3crab 2899 . . 3 class {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}
252, 4, 24cmpt 4637 . 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
261, 25wceq 1474 1 wff IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
Colors of variables: wff setvar class
This definition is referenced by:  itgoval  36533  itgocn  36536
  Copyright terms: Public domain W3C validator