Definition df-itgo 43102

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 43105. 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 43100	. 2 class IntgOver
2		vs	. . 3 setvar 𝑠
3		cc 11144	. . . 4 class ℂ
4	3	cpw 4604	. . 3 class 𝒫 ℂ
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1534	. . . . . . . 8 class 𝑥
7		vp	. . . . . . . . 9 setvar 𝑝
8	7	cv 1534	. . . . . . . 8 class 𝑝
9	6, 8	cfv 6558	. . . . . . 7 class (𝑝‘𝑥)
10		cc0 11146	. . . . . . 7 class 0
11	9, 10	wceq 1535	. . . . . 6 wff (𝑝‘𝑥) = 0
12		cdgr 26222	. . . . . . . . 9 class deg
13	8, 12	cfv 6558	. . . . . . . 8 class (deg‘𝑝)
14		ccoe 26221	. . . . . . . . 9 class coeff
15	8, 14	cfv 6558	. . . . . . . 8 class (coeff‘𝑝)
16	13, 15	cfv 6558	. . . . . . 7 class ((coeff‘𝑝)‘(deg‘𝑝))
17		c1 11147	. . . . . . 7 class 1
18	16, 17	wceq 1535	. . . . . 6 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
19	11, 18	wa 395	. . . . 5 wff ((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
20	2	cv 1534	. . . . . 6 class 𝑠
21		cply 26219	. . . . . 6 class Poly
22	20, 21	cfv 6558	. . . . 5 class (Poly‘𝑠)
23	19, 7, 22	wrex 3066	. . . 4 wff ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
24	23, 5, 3	crab 3432	. . 3 class {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}
25	2, 4, 24	cmpt 5232	. 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
26	1, 25	wceq 1535	1 wff IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})

This definition is referenced by:  itgoval  43104  itgocn  43107