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 40687
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 40690. 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 40685 . 2 class IntgOver
2 vs . . 3 setvar 𝑠
3 cc 10727 . . . 4 class
43cpw 4513 . . 3 class 𝒫 ℂ
5 vx . . . . . . . . 9 setvar 𝑥
65cv 1542 . . . . . . . 8 class 𝑥
7 vp . . . . . . . . 9 setvar 𝑝
87cv 1542 . . . . . . . 8 class 𝑝
96, 8cfv 6380 . . . . . . 7 class (𝑝𝑥)
10 cc0 10729 . . . . . . 7 class 0
119, 10wceq 1543 . . . . . 6 wff (𝑝𝑥) = 0
12 cdgr 25081 . . . . . . . . 9 class deg
138, 12cfv 6380 . . . . . . . 8 class (deg‘𝑝)
14 ccoe 25080 . . . . . . . . 9 class coeff
158, 14cfv 6380 . . . . . . . 8 class (coeff‘𝑝)
1613, 15cfv 6380 . . . . . . 7 class ((coeff‘𝑝)‘(deg‘𝑝))
17 c1 10730 . . . . . . 7 class 1
1816, 17wceq 1543 . . . . . 6 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
1911, 18wa 399 . . . . 5 wff ((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
202cv 1542 . . . . . 6 class 𝑠
21 cply 25078 . . . . . 6 class Poly
2220, 21cfv 6380 . . . . 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 5135 . 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
261, 25wceq 1543 1 wff IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
Colors of variables: wff setvar class
This definition is referenced by:  itgoval  40689  itgocn  40692
  Copyright terms: Public domain W3C validator