Definition df-itgo 40984

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 40987. 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 40982	. 2 class IntgOver
2		vs	. . 3 setvar 𝑠
3		cc 10869	. . . 4 class ℂ
4	3	cpw 4533	. . 3 class 𝒫 ℂ
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1538	. . . . . . . 8 class 𝑥
7		vp	. . . . . . . . 9 setvar 𝑝
8	7	cv 1538	. . . . . . . 8 class 𝑝
9	6, 8	cfv 6433	. . . . . . 7 class (𝑝‘𝑥)
10		cc0 10871	. . . . . . 7 class 0
11	9, 10	wceq 1539	. . . . . 6 wff (𝑝‘𝑥) = 0
12		cdgr 25348	. . . . . . . . 9 class deg
13	8, 12	cfv 6433	. . . . . . . 8 class (deg‘𝑝)
14		ccoe 25347	. . . . . . . . 9 class coeff
15	8, 14	cfv 6433	. . . . . . . 8 class (coeff‘𝑝)
16	13, 15	cfv 6433	. . . . . . 7 class ((coeff‘𝑝)‘(deg‘𝑝))
17		c1 10872	. . . . . . 7 class 1
18	16, 17	wceq 1539	. . . . . 6 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
19	11, 18	wa 396	. . . . 5 wff ((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
20	2	cv 1538	. . . . . 6 class 𝑠
21		cply 25345	. . . . . 6 class Poly
22	20, 21	cfv 6433	. . . . 5 class (Poly‘𝑠)
23	19, 7, 22	wrex 3065	. . . 4 wff ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
24	23, 5, 3	crab 3068	. . 3 class {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}
25	2, 4, 24	cmpt 5157	. 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
26	1, 25	wceq 1539	1 wff IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})

This definition is referenced by:  itgoval  40986  itgocn  40989