Definition df-itgo 43276

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 43279. 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 43274	. 2 class IntgOver
2		vs	. . 3 setvar 𝑠
3		cc 11011	. . . 4 class ℂ
4	3	cpw 4549	. . 3 class 𝒫 ℂ
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1540	. . . . . . . 8 class 𝑥
7		vp	. . . . . . . . 9 setvar 𝑝
8	7	cv 1540	. . . . . . . 8 class 𝑝
9	6, 8	cfv 6486	. . . . . . 7 class (𝑝‘𝑥)
10		cc0 11013	. . . . . . 7 class 0
11	9, 10	wceq 1541	. . . . . 6 wff (𝑝‘𝑥) = 0
12		cdgr 26120	. . . . . . . . 9 class deg
13	8, 12	cfv 6486	. . . . . . . 8 class (deg‘𝑝)
14		ccoe 26119	. . . . . . . . 9 class coeff
15	8, 14	cfv 6486	. . . . . . . 8 class (coeff‘𝑝)
16	13, 15	cfv 6486	. . . . . . 7 class ((coeff‘𝑝)‘(deg‘𝑝))
17		c1 11014	. . . . . . 7 class 1
18	16, 17	wceq 1541	. . . . . 6 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
19	11, 18	wa 395	. . . . 5 wff ((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
20	2	cv 1540	. . . . . 6 class 𝑠
21		cply 26117	. . . . . 6 class Poly
22	20, 21	cfv 6486	. . . . 5 class (Poly‘𝑠)
23	19, 7, 22	wrex 3057	. . . 4 wff ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
24	23, 5, 3	crab 3396	. . 3 class {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}
25	2, 4, 24	cmpt 5174	. 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
26	1, 25	wceq 1541	1 wff IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})

This definition is referenced by:  itgoval  43278  itgocn  43281