Definition df-itgo 43149

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 43152. 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 43147	. 2 class IntgOver
2		vs	. . 3 setvar 𝑠
3		cc 11149	. . . 4 class ℂ
4	3	cpw 4598	. . 3 class 𝒫 ℂ
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1539	. . . . . . . 8 class 𝑥
7		vp	. . . . . . . . 9 setvar 𝑝
8	7	cv 1539	. . . . . . . 8 class 𝑝
9	6, 8	cfv 6559	. . . . . . 7 class (𝑝‘𝑥)
10		cc0 11151	. . . . . . 7 class 0
11	9, 10	wceq 1540	. . . . . 6 wff (𝑝‘𝑥) = 0
12		cdgr 26216	. . . . . . . . 9 class deg
13	8, 12	cfv 6559	. . . . . . . 8 class (deg‘𝑝)
14		ccoe 26215	. . . . . . . . 9 class coeff
15	8, 14	cfv 6559	. . . . . . . 8 class (coeff‘𝑝)
16	13, 15	cfv 6559	. . . . . . 7 class ((coeff‘𝑝)‘(deg‘𝑝))
17		c1 11152	. . . . . . 7 class 1
18	16, 17	wceq 1540	. . . . . 6 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
19	11, 18	wa 395	. . . . 5 wff ((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
20	2	cv 1539	. . . . . 6 class 𝑠
21		cply 26213	. . . . . 6 class Poly
22	20, 21	cfv 6559	. . . . 5 class (Poly‘𝑠)
23	19, 7, 22	wrex 3069	. . . 4 wff ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
24	23, 5, 3	crab 3435	. . 3 class {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}
25	2, 4, 24	cmpt 5223	. 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
26	1, 25	wceq 1540	1 wff IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})

This definition is referenced by:  itgoval  43151  itgocn  43154