Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-itgo Unicode version

Definition df-itgo 27467
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 27470. 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
StepHypRef Expression
1 citgo 27465 . 2  class IntgOver
2 vs . . 3  set  s
3 cc 8751 . . . 4  class  CC
43cpw 3638 . . 3  class  ~P CC
5 vx . . . . . . . . 9  set  x
65cv 1631 . . . . . . . 8  class  x
7 vp . . . . . . . . 9  set  p
87cv 1631 . . . . . . . 8  class  p
96, 8cfv 5271 . . . . . . 7  class  ( p `
 x )
10 cc0 8753 . . . . . . 7  class  0
119, 10wceq 1632 . . . . . 6  wff  ( p `
 x )  =  0
12 cdgr 19585 . . . . . . . . 9  class deg
138, 12cfv 5271 . . . . . . . 8  class  (deg `  p )
14 ccoe 19584 . . . . . . . . 9  class coeff
158, 14cfv 5271 . . . . . . . 8  class  (coeff `  p )
1613, 15cfv 5271 . . . . . . 7  class  ( (coeff `  p ) `  (deg `  p ) )
17 c1 8754 . . . . . . 7  class  1
1816, 17wceq 1632 . . . . . 6  wff  ( (coeff `  p ) `  (deg `  p ) )  =  1
1911, 18wa 358 . . . . 5  wff  ( ( p `  x )  =  0  /\  (
(coeff `  p ) `  (deg `  p )
)  =  1 )
202cv 1631 . . . . . 6  class  s
21 cply 19582 . . . . . 6  class Poly
2220, 21cfv 5271 . . . . 5  class  (Poly `  s )
2319, 7, 22wrex 2557 . . . 4  wff  E. p  e.  (Poly `  s )
( ( p `  x )  =  0  /\  ( (coeff `  p ) `  (deg `  p ) )  =  1 )
2423, 5, 3crab 2560 . . 3  class  { x  e.  CC  |  E. p  e.  (Poly `  s )
( ( p `  x )  =  0  /\  ( (coeff `  p ) `  (deg `  p ) )  =  1 ) }
252, 4, 24cmpt 4093 . 2  class  ( s  e.  ~P CC  |->  { x  e.  CC  |  E. p  e.  (Poly `  s ) ( ( p `  x )  =  0  /\  (
(coeff `  p ) `  (deg `  p )
)  =  1 ) } )
261, 25wceq 1632 1  wff IntgOver  =  ( s  e.  ~P CC  |->  { x  e.  CC  |  E. p  e.  (Poly `  s ) ( ( p `  x )  =  0  /\  (
(coeff `  p ) `  (deg `  p )
)  =  1 ) } )
Colors of variables: wff set class
This definition is referenced by:  itgoval  27469  itgocn  27472
  Copyright terms: Public domain W3C validator