Definition df-itgo 43611

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 43614. 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 43609	. 2 class IntgOver
2		vs	. . 3 setvar 𝑠
3		cc 11034	. . . 4 class ℂ
4	3	cpw 4536	. . 3 class 𝒫 ℂ
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1546	. . . . . . . 8 class 𝑥
7		vp	. . . . . . . . 9 setvar 𝑝
8	7	cv 1546	. . . . . . . 8 class 𝑝
9	6, 8	cfv 6492	. . . . . . 7 class (𝑝‘𝑥)
10		cc0 11036	. . . . . . 7 class 0
11	9, 10	wceq 1547	. . . . . 6 wff (𝑝‘𝑥) = 0
12		cdgr 26177	. . . . . . . . 9 class deg
13	8, 12	cfv 6492	. . . . . . . 8 class (deg‘𝑝)
14		ccoe 26176	. . . . . . . . 9 class coeff
15	8, 14	cfv 6492	. . . . . . . 8 class (coeff‘𝑝)
16	13, 15	cfv 6492	. . . . . . 7 class ((coeff‘𝑝)‘(deg‘𝑝))
17		c1 11037	. . . . . . 7 class 1
18	16, 17	wceq 1547	. . . . . 6 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
19	11, 18	wa 396	. . . . 5 wff ((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
20	2	cv 1546	. . . . . 6 class 𝑠
21		cply 26174	. . . . . 6 class Poly
22	20, 21	cfv 6492	. . . . 5 class (Poly‘𝑠)
23	19, 7, 22	wrex 3064	. . . 4 wff ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)
24	23, 5, 3	crab 3392	. . 3 class {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)}
25	2, 4, 24	cmpt 5160	. 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})
26	1, 25	wceq 1547	1 wff IntgOver = (𝑠 ∈ 𝒫 ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑝 ∈ (Poly‘𝑠)((𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(deg‘𝑝)) = 1)})

This definition is referenced by:  itgoval  43613  itgocn  43616