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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		citgo	|- IntgOver
1		vs	|- s
2		cc	|- CC
3	2	cpw	|- ~P CC
4		vx	|- x
5		vp	|- p
6		cply	|- Poly
7	1	cv	|- s
8	7 6	cfv	|- ( Poly ` s )
9	5	cv	|- p
10	4	cv	|- x
11	10 9	cfv	|- ( p ` x )
12		cc0	|- 0
13	11 12	wceq	|- ( p ` x ) = 0
14		ccoe	|- coeff
15	9 14	cfv	|- ( coeff ` p )
16		cdgr	|- deg
17	9 16	cfv	|- ( deg ` p )
18	17 15	cfv	|- ( ( coeff ` p ) ` ( deg ` p ) )
19		c1	|- 1
20	18 19	wceq	|- ( ( coeff ` p ) ` ( deg ` p ) ) = 1
21	13 20	wa	|- ( ( p ` x ) = 0 /\ ( ( coeff ` p ) ` ( deg ` p ) ) = 1 )
22	21 5 8	wrex	|- E. p e. ( Poly ` s ) ( ( p ` x ) = 0 /\ ( ( coeff ` p ) ` ( deg ` p ) ) = 1 )
23	22 4 2	crab	|- { x e. CC | E. p e. ( Poly ` s ) ( ( p ` x ) = 0 /\ ( ( coeff ` p ) ` ( deg ` p ) ) = 1 ) }
24	1 3 23	cmpt	|- ( s e. ~P CC |-> { x e. CC | E. p e. ( Poly ` s ) ( ( p ` x ) = 0 /\ ( ( coeff ` p ) ` ( deg ` p ) ) = 1 ) } )
25	0 24	wceq	|- IntgOver = ( s e. ~P CC |-> { x e. CC | E. p e. ( Poly ` s ) ( ( p ` x ) = 0 /\ ( ( coeff ` p ) ` ( deg ` p ) ) = 1 ) } )