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

Definition df-itgo 27343
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 27346. 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 27341 . 2  class IntgOver
2 vs . . 3  set  s
3 cc 8990 . . . 4  class  CC
43cpw 3801 . . 3  class  ~P CC
5 vx . . . . . . . . 9  set  x
65cv 1652 . . . . . . . 8  class  x
7 vp . . . . . . . . 9  set  p
87cv 1652 . . . . . . . 8  class  p
96, 8cfv 5456 . . . . . . 7  class  ( p `
 x )
10 cc0 8992 . . . . . . 7  class  0
119, 10wceq 1653 . . . . . 6  wff  ( p `
 x )  =  0
12 cdgr 20108 . . . . . . . . 9  class deg
138, 12cfv 5456 . . . . . . . 8  class  (deg `  p )
14 ccoe 20107 . . . . . . . . 9  class coeff
158, 14cfv 5456 . . . . . . . 8  class  (coeff `  p )
1613, 15cfv 5456 . . . . . . 7  class  ( (coeff `  p ) `  (deg `  p ) )
17 c1 8993 . . . . . . 7  class  1
1816, 17wceq 1653 . . . . . 6  wff  ( (coeff `  p ) `  (deg `  p ) )  =  1
1911, 18wa 360 . . . . 5  wff  ( ( p `  x )  =  0  /\  (
(coeff `  p ) `  (deg `  p )
)  =  1 )
202cv 1652 . . . . . 6  class  s
21 cply 20105 . . . . . 6  class Poly
2220, 21cfv 5456 . . . . 5  class  (Poly `  s )
2319, 7, 22wrex 2708 . . . 4  wff  E. p  e.  (Poly `  s )
( ( p `  x )  =  0  /\  ( (coeff `  p ) `  (deg `  p ) )  =  1 )
2423, 5, 3crab 2711 . . 3  class  { x  e.  CC  |  E. p  e.  (Poly `  s )
( ( p `  x )  =  0  /\  ( (coeff `  p ) `  (deg `  p ) )  =  1 ) }
252, 4, 24cmpt 4268 . 2  class  ( s  e.  ~P CC  |->  { x  e.  CC  |  E. p  e.  (Poly `  s ) ( ( p `  x )  =  0  /\  (
(coeff `  p ) `  (deg `  p )
)  =  1 ) } )
261, 25wceq 1653 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  27345  itgocn  27348
  Copyright terms: Public domain W3C validator