Definition df-itgo 39265

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 39268. 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 39263	. 2 class IntgOver
2		vs	. . 3 setvar 𝑠
3		cc 10388	. . . 4 class ℂ
4	3	cpw 4459	. . 3 class 𝒫 ℂ
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1524	. . . . . . . 8 class 𝑥
7		vp	. . . . . . . . 9 setvar 𝑝
8	7	cv 1524	. . . . . . . 8 class 𝑝
9	6, 8	cfv 6232	. . . . . . 7 class (𝑝‘𝑥)
10		cc0 10390	. . . . . . 7 class 0
11	9, 10	wceq 1525	. . . . . 6 wff (𝑝‘𝑥) = 0
12		cdgr 24464	. . . . . . . . 9 class deg
13	8, 12	cfv 6232	. . . . . . . 8 class (deg‘𝑝)
14		ccoe 24463	. . . . . . . . 9 class coeff
15	8, 14	cfv 6232	. . . . . . . 8 class (coeff‘𝑝)
16	13, 15	cfv 6232	. . . . . . 7 class ((coeff‘𝑝)‘(deg‘𝑝))
17		c1 10391	. . . . . . 7 class 1
18	16, 17	wceq 1525	. . . . . 6 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
19	11, 18	wa 396	. . . . 5 wff ((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
20	2	cv 1524	. . . . . 6 class 𝑠
21		cply 24461	. . . . . 6 class Poly
22	20, 21	cfv 6232	. . . . 5 class (Poly‘𝑠)
23	19, 7, 22	wrex 3108	. . . 4 wff ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
24	23, 5, 3	crab 3111	. . 3 class {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}
25	2, 4, 24	cmpt 5047	. 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
26	1, 25	wceq 1525	1 wff IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})

This definition is referenced by:  itgoval  39267  itgocn  39270