Definition df-itgo 43696

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 43699. 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

Step	Hyp	Ref	Expression
1		citgo 43694	. 2 class IntgOver
2		vs	. . 3 setvar 𝑠
3		cc 11064	. . . 4 class ℂ
4	3	cpw 4552	. . 3 class 𝒫 ℂ
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1558	. . . . . . . 8 class 𝑥
7		vp	. . . . . . . . 9 setvar 𝑝
8	7	cv 1558	. . . . . . . 8 class 𝑝
9	6, 8	cfv 6515	. . . . . . 7 class (𝑝‘𝑥)
10		cc0 11066	. . . . . . 7 class 0
11	9, 10	wceq 1559	. . . . . 6 wff (𝑝‘𝑥) = 0
12		cdgr 26234	. . . . . . . . 9 class deg
13	8, 12	cfv 6515	. . . . . . . 8 class (deg‘𝑝)
14		ccoe 26233	. . . . . . . . 9 class coeff
15	8, 14	cfv 6515	. . . . . . . 8 class (coeff‘𝑝)
16	13, 15	cfv 6515	. . . . . . 7 class ((coeff‘𝑝)‘(deg‘𝑝))
17		c1 11067	. . . . . . 7 class 1
18	16, 17	wceq 1559	. . . . . 6 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
19	11, 18	wa 399	. . . . 5 wff ((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
20	2	cv 1558	. . . . . 6 class 𝑠
21		cply 26231	. . . . . 6 class Poly
22	20, 21	cfv 6515	. . . . 5 class (Poly‘𝑠)
23	19, 7, 22	wrex 3085	. . . 4 wff ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
24	23, 5, 3	crab 3413	. . 3 class {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}
25	2, 4, 24	cmpt 5178	. 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
26	1, 25	wceq 1559	1 wff IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})

This definition is referenced by:  itgoval  43698  itgocn  43701