Definition df-itgo 41901

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 41904. 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 41899	. 2 class IntgOver
2		vs	. . 3 setvar 𝑠
3		cc 11108	. . . 4 class ℂ
4	3	cpw 4603	. . 3 class 𝒫 ℂ
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1541	. . . . . . . 8 class 𝑥
7		vp	. . . . . . . . 9 setvar 𝑝
8	7	cv 1541	. . . . . . . 8 class 𝑝
9	6, 8	cfv 6544	. . . . . . 7 class (𝑝‘𝑥)
10		cc0 11110	. . . . . . 7 class 0
11	9, 10	wceq 1542	. . . . . 6 wff (𝑝‘𝑥) = 0
12		cdgr 25701	. . . . . . . . 9 class deg
13	8, 12	cfv 6544	. . . . . . . 8 class (deg‘𝑝)
14		ccoe 25700	. . . . . . . . 9 class coeff
15	8, 14	cfv 6544	. . . . . . . 8 class (coeff‘𝑝)
16	13, 15	cfv 6544	. . . . . . 7 class ((coeff‘𝑝)‘(deg‘𝑝))
17		c1 11111	. . . . . . 7 class 1
18	16, 17	wceq 1542	. . . . . 6 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
19	11, 18	wa 397	. . . . 5 wff ((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
20	2	cv 1541	. . . . . 6 class 𝑠
21		cply 25698	. . . . . 6 class Poly
22	20, 21	cfv 6544	. . . . 5 class (Poly‘𝑠)
23	19, 7, 22	wrex 3071	. . . 4 wff ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
24	23, 5, 3	crab 3433	. . 3 class {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}
25	2, 4, 24	cmpt 5232	. 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
26	1, 25	wceq 1542	1 wff IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})

This definition is referenced by:  itgoval  41903  itgocn  41906