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 27364
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 27367. 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 27362 . 2  class IntgOver
2 vs . . 3  set  s
3 cc 8735 . . . 4  class  CC
43cpw 3625 . . 3  class  ~P CC
5 vx . . . . . . . . 9  set  x
65cv 1622 . . . . . . . 8  class  x
7 vp . . . . . . . . 9  set  p
87cv 1622 . . . . . . . 8  class  p
96, 8cfv 5255 . . . . . . 7  class  ( p `
 x )
10 cc0 8737 . . . . . . 7  class  0
119, 10wceq 1623 . . . . . 6  wff  ( p `
 x )  =  0
12 cdgr 19569 . . . . . . . . 9  class deg
138, 12cfv 5255 . . . . . . . 8  class  (deg `  p )
14 ccoe 19568 . . . . . . . . 9  class coeff
158, 14cfv 5255 . . . . . . . 8  class  (coeff `  p )
1613, 15cfv 5255 . . . . . . 7  class  ( (coeff `  p ) `  (deg `  p ) )
17 c1 8738 . . . . . . 7  class  1
1816, 17wceq 1623 . . . . . 6  wff  ( (coeff `  p ) `  (deg `  p ) )  =  1
1911, 18wa 358 . . . . 5  wff  ( ( p `  x )  =  0  /\  (
(coeff `  p ) `  (deg `  p )
)  =  1 )
202cv 1622 . . . . . 6  class  s
21 cply 19566 . . . . . 6  class Poly
2220, 21cfv 5255 . . . . 5  class  (Poly `  s )
2319, 7, 22wrex 2544 . . . 4  wff  E. p  e.  (Poly `  s )
( ( p `  x )  =  0  /\  ( (coeff `  p ) `  (deg `  p ) )  =  1 )
2423, 5, 3crab 2547 . . 3  class  { x  e.  CC  |  E. p  e.  (Poly `  s )
( ( p `  x )  =  0  /\  ( (coeff `  p ) `  (deg `  p ) )  =  1 ) }
252, 4, 24cmpt 4077 . 2  class  ( s  e.  ~P CC  |->  { x  e.  CC  |  E. p  e.  (Poly `  s ) ( ( p `  x )  =  0  /\  (
(coeff `  p ) `  (deg `  p )
)  =  1 ) } )
261, 25wceq 1623 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  27366  itgocn  27369
  Copyright terms: Public domain W3C validator