Definition df-itgo 44145

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 44148. 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 44143	. 2 class IntgOver
2		vs	. . 3 setvar 𝑠
3		cc 11191	. . . 4 class ℂ
4	3	cpw 4557	. . 3 class 𝒫 ℂ
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1569	. . . . . . . 8 class 𝑥
7		vp	. . . . . . . . 9 setvar 𝑝
8	7	cv 1569	. . . . . . . 8 class 𝑝
9	6, 8	cfv 6537	. . . . . . 7 class (𝑝‘𝑥)
10		cc0 11193	. . . . . . 7 class 0
11	9, 10	wceq 1570	. . . . . 6 wff (𝑝‘𝑥) = 0
12		cdgr 26498	. . . . . . . . 9 class deg
13	8, 12	cfv 6537	. . . . . . . 8 class (deg‘𝑝)
14		ccoe 26497	. . . . . . . . 9 class coeff
15	8, 14	cfv 6537	. . . . . . . 8 class (coeff‘𝑝)
16	13, 15	cfv 6537	. . . . . . 7 class ((coeff‘𝑝)‘(deg‘𝑝))
17		c1 11194	. . . . . . 7 class 1
18	16, 17	wceq 1570	. . . . . 6 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
19	11, 18	wa 401	. . . . 5 wff ((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
20	2	cv 1569	. . . . . 6 class 𝑠
21		cply 26495	. . . . . 6 class Poly
22	20, 21	cfv 6537	. . . . 5 class (Poly‘𝑠)
23	19, 7, 22	wrex 3087	. . . 4 wff ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
24	23, 5, 3	crab 3413	. . 3 class {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}
25	2, 4, 24	cmpt 5186	. 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
26	1, 25	wceq 1570	1 wff IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})

This definition is used by:  itgoval  44147  itgocn  44150