Definition df-itgo 44255

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 44258. 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 44253	. 2 class IntgOver
2		vs	. . 3 setvar 𝑠
3		cc 11202	. . . 4 class ℂ
4	3	cpw 4556	. . 3 class 𝒫 ℂ
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1568	. . . . . . . 8 class 𝑥
7		vp	. . . . . . . . 9 setvar 𝑝
8	7	cv 1568	. . . . . . . 8 class 𝑝
9	6, 8	cfv 6539	. . . . . . 7 class (𝑝‘𝑥)
10		cc0 11204	. . . . . . 7 class 0
11	9, 10	wceq 1569	. . . . . 6 wff (𝑝‘𝑥) = 0
12		cdgr 26511	. . . . . . . . 9 class deg
13	8, 12	cfv 6539	. . . . . . . 8 class (deg‘𝑝)
14		ccoe 26510	. . . . . . . . 9 class coeff
15	8, 14	cfv 6539	. . . . . . . 8 class (coeff‘𝑝)
16	13, 15	cfv 6539	. . . . . . 7 class ((coeff‘𝑝)‘(deg‘𝑝))
17		c1 11205	. . . . . . 7 class 1
18	16, 17	wceq 1569	. . . . . 6 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
19	11, 18	wa 401	. . . . 5 wff ((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
20	2	cv 1568	. . . . . 6 class 𝑠
21		cply 26508	. . . . . 6 class Poly
22	20, 21	cfv 6539	. . . . 5 class (Poly‘𝑠)
23	19, 7, 22	wrex 3086	. . . 4 wff ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
24	23, 5, 3	crab 3412	. . 3 class {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}
25	2, 4, 24	cmpt 5185	. 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
26	1, 25	wceq 1569	1 wff IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})

This definition is used by:  itgoval  44257  itgocn  44260