Definition df-itgo 37729

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 37732. 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 = ( s e. ~P CC |-> { x e. CC | E. p e. (Poly ` s ) ( ( p ` x ) = 0 /\ ( (coeff ` p ) ` (deg ` p ) ) = 1 ) } )

Distinct variable group:   x, p, s

Detailed syntax breakdown of Definition df-itgo

Step	Hyp	Ref	Expression
1		citgo 37727	. 2 class IntgOver
2		vs	. . 3 setvar s
3		cc 9934	. . . 4 class CC
4	3	cpw 4158	. . 3 class ~P CC
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1482	. . . . . . . 8 class x
7		vp	. . . . . . . . 9 setvar p
8	7	cv 1482	. . . . . . . 8 class p
9	6, 8	cfv 5888	. . . . . . 7 class ( p ` x )
10		cc0 9936	. . . . . . 7 class 0
11	9, 10	wceq 1483	. . . . . 6 wff ( p ` x ) = 0
12		cdgr 23943	. . . . . . . . 9 class deg
13	8, 12	cfv 5888	. . . . . . . 8 class (deg ` p )
14		ccoe 23942	. . . . . . . . 9 class coeff
15	8, 14	cfv 5888	. . . . . . . 8 class (coeff ` p )
16	13, 15	cfv 5888	. . . . . . 7 class ( (coeff ` p ) ` (deg ` p ) )
17		c1 9937	. . . . . . 7 class 1
18	16, 17	wceq 1483	. . . . . 6 wff ( (coeff ` p ) ` (deg ` p ) ) = 1
19	11, 18	wa 384	. . . . 5 wff ( ( p ` x ) = 0 /\ ( (coeff ` p ) ` (deg ` p ) ) = 1 )
20	2	cv 1482	. . . . . 6 class s
21		cply 23940	. . . . . 6 class Poly
22	20, 21	cfv 5888	. . . . 5 class (Poly ` s )
23	19, 7, 22	wrex 2913	. . . 4 wff E. p e. (Poly ` s ) ( ( p ` x ) = 0 /\ ( (coeff ` p ) ` (deg ` p ) ) = 1 )
24	23, 5, 3	crab 2916	. . 3 class { x e. CC | E. p e. (Poly ` s ) ( ( p ` x ) = 0 /\ ( (coeff ` p ) ` (deg ` p ) ) = 1 ) }
25	2, 4, 24	cmpt 4729	. 2 class ( s e. ~P CC |-> { x e. CC | E. p e. (Poly ` s ) ( ( p ` x ) = 0 /\ ( (coeff ` p ) ` (deg ` p ) ) = 1 ) } )
26	1, 25	wceq 1483	1 wff IntgOver = ( s e. ~P CC |-> { x e. CC | E. p e. (Poly ` s ) ( ( p ` x ) = 0 /\ ( (coeff ` p ) ` (deg ` p ) ) = 1 ) } )

This definition is referenced by:  itgoval  37731  itgocn  37734