Definition df-itgo 36748

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 36751. 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 36746	. 2 class IntgOver
2		vs	. . 3 setvar 𝑠
3		cc 9813	. . . 4 class ℂ
4	3	cpw 4108	. . 3 class 𝒫 ℂ
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1474	. . . . . . . 8 class 𝑥
7		vp	. . . . . . . . 9 setvar 𝑝
8	7	cv 1474	. . . . . . . 8 class 𝑝
9	6, 8	cfv 5804	. . . . . . 7 class (𝑝‘𝑥)
10		cc0 9815	. . . . . . 7 class 0
11	9, 10	wceq 1475	. . . . . 6 wff (𝑝‘𝑥) = 0
12		cdgr 23747	. . . . . . . . 9 class deg
13	8, 12	cfv 5804	. . . . . . . 8 class (deg‘𝑝)
14		ccoe 23746	. . . . . . . . 9 class coeff
15	8, 14	cfv 5804	. . . . . . . 8 class (coeff‘𝑝)
16	13, 15	cfv 5804	. . . . . . 7 class ((coeff‘𝑝)‘(deg‘𝑝))
17		c1 9816	. . . . . . 7 class 1
18	16, 17	wceq 1475	. . . . . 6 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
19	11, 18	wa 383	. . . . 5 wff ((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
20	2	cv 1474	. . . . . 6 class 𝑠
21		cply 23744	. . . . . 6 class Poly
22	20, 21	cfv 5804	. . . . 5 class (Poly‘𝑠)
23	19, 7, 22	wrex 2897	. . . 4 wff ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
24	23, 5, 3	crab 2900	. . 3 class {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}
25	2, 4, 24	cmpt 4643	. 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
26	1, 25	wceq 1475	1 wff IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})

This definition is referenced by:  itgoval  36750  itgocn  36753