Definition df-itgo 39766

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 39769. 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 39764	. 2 class IntgOver
2		vs	. . 3 setvar 𝑠
3		cc 10537	. . . 4 class ℂ
4	3	cpw 4541	. . 3 class 𝒫 ℂ
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1536	. . . . . . . 8 class 𝑥
7		vp	. . . . . . . . 9 setvar 𝑝
8	7	cv 1536	. . . . . . . 8 class 𝑝
9	6, 8	cfv 6357	. . . . . . 7 class (𝑝‘𝑥)
10		cc0 10539	. . . . . . 7 class 0
11	9, 10	wceq 1537	. . . . . 6 wff (𝑝‘𝑥) = 0
12		cdgr 24779	. . . . . . . . 9 class deg
13	8, 12	cfv 6357	. . . . . . . 8 class (deg‘𝑝)
14		ccoe 24778	. . . . . . . . 9 class coeff
15	8, 14	cfv 6357	. . . . . . . 8 class (coeff‘𝑝)
16	13, 15	cfv 6357	. . . . . . 7 class ((coeff‘𝑝)‘(deg‘𝑝))
17		c1 10540	. . . . . . 7 class 1
18	16, 17	wceq 1537	. . . . . 6 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
19	11, 18	wa 398	. . . . 5 wff ((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
20	2	cv 1536	. . . . . 6 class 𝑠
21		cply 24776	. . . . . 6 class Poly
22	20, 21	cfv 6357	. . . . 5 class (Poly‘𝑠)
23	19, 7, 22	wrex 3141	. . . 4 wff ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
24	23, 5, 3	crab 3144	. . 3 class {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}
25	2, 4, 24	cmpt 5148	. 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
26	1, 25	wceq 1537	1 wff IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})

This definition is referenced by:  itgoval  39768  itgocn  39771