Definition df-itgo 40687

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 40690. 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 40685	. 2 class IntgOver
2		vs	. . 3 setvar 𝑠
3		cc 10727	. . . 4 class ℂ
4	3	cpw 4513	. . 3 class 𝒫 ℂ
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1542	. . . . . . . 8 class 𝑥
7		vp	. . . . . . . . 9 setvar 𝑝
8	7	cv 1542	. . . . . . . 8 class 𝑝
9	6, 8	cfv 6380	. . . . . . 7 class (𝑝‘𝑥)
10		cc0 10729	. . . . . . 7 class 0
11	9, 10	wceq 1543	. . . . . 6 wff (𝑝‘𝑥) = 0
12		cdgr 25081	. . . . . . . . 9 class deg
13	8, 12	cfv 6380	. . . . . . . 8 class (deg‘𝑝)
14		ccoe 25080	. . . . . . . . 9 class coeff
15	8, 14	cfv 6380	. . . . . . . 8 class (coeff‘𝑝)
16	13, 15	cfv 6380	. . . . . . 7 class ((coeff‘𝑝)‘(deg‘𝑝))
17		c1 10730	. . . . . . 7 class 1
18	16, 17	wceq 1543	. . . . . 6 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
19	11, 18	wa 399	. . . . 5 wff ((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
20	2	cv 1542	. . . . . 6 class 𝑠
21		cply 25078	. . . . . 6 class Poly
22	20, 21	cfv 6380	. . . . 5 class (Poly‘𝑠)
23	19, 7, 22	wrex 3062	. . . 4 wff ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
24	23, 5, 3	crab 3065	. . 3 class {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}
25	2, 4, 24	cmpt 5135	. 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
26	1, 25	wceq 1543	1 wff IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})

This definition is referenced by:  itgoval  40689  itgocn  40692