Definition df-itgo

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 . 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)

	Ref	Expression
Assertion	df-itgo	⊢ IntgOver = ( 𝑠 ∈ 𝒫 ℂ ↦ { 𝑥 ∈ ℂ ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝑠 ) ( ( 𝑝 ‘ 𝑥 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		citgo	⊢ IntgOver
1		vs	⊢ 𝑠
2		cc	⊢ ℂ
3	2	cpw	⊢ 𝒫 ℂ
4		vx	⊢ 𝑥
5		vp	⊢ 𝑝
6		cply	⊢ Poly
7	1	cv	⊢ 𝑠
8	7 6	cfv	⊢ ( Poly ‘ 𝑠 )
9	5	cv	⊢ 𝑝
10	4	cv	⊢ 𝑥
11	10 9	cfv	⊢ ( 𝑝 ‘ 𝑥 )
12		cc0	⊢ 0
13	11 12	wceq	⊢ ( 𝑝 ‘ 𝑥 ) = 0
14		ccoe	⊢ coeff
15	9 14	cfv	⊢ ( coeff ‘ 𝑝 )
16		cdgr	⊢ deg
17	9 16	cfv	⊢ ( deg ‘ 𝑝 )
18	17 15	cfv	⊢ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) )
19		c1	⊢ 1
20	18 19	wceq	⊢ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1
21	13 20	wa	⊢ ( ( 𝑝 ‘ 𝑥 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 )
22	21 5 8	wrex	⊢ ∃ 𝑝 ∈ ( Poly ‘ 𝑠 ) ( ( 𝑝 ‘ 𝑥 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 )
23	22 4 2	crab	⊢ { 𝑥 ∈ ℂ ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝑠 ) ( ( 𝑝 ‘ 𝑥 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 ) }
24	1 3 23	cmpt	⊢ ( 𝑠 ∈ 𝒫 ℂ ↦ { 𝑥 ∈ ℂ ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝑠 ) ( ( 𝑝 ‘ 𝑥 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 ) } )
25	0 24	wceq	⊢ IntgOver = ( 𝑠 ∈ 𝒫 ℂ ↦ { 𝑥 ∈ ℂ ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝑠 ) ( ( 𝑝 ‘ 𝑥 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 ) } )