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

Definition df-mpaa 27348
Description: Define the minimal polynomial of an algebraic number as the unique monic polynomial which achieves the minimum of degAA. (Contributed by Stefan O'Rear, 25-Nov-2014.)
Assertion
Ref Expression
df-mpaa  |- minPolyAA  =  ( x  e.  AA  |->  (
iota_ p  e.  (Poly `  QQ ) ( (deg
`  p )  =  (degAA `  x )  /\  ( p `  x
)  =  0  /\  ( (coeff `  p
) `  (degAA `  x
) )  =  1 ) ) )
Distinct variable group:    x, p

Detailed syntax breakdown of Definition df-mpaa
StepHypRef Expression
1 cmpaa 27346 . 2  class minPolyAA
2 vx . . 3  set  x
3 caa 19694 . . 3  class  AA
4 vp . . . . . . . 8  set  p
54cv 1622 . . . . . . 7  class  p
6 cdgr 19569 . . . . . . 7  class deg
75, 6cfv 5255 . . . . . 6  class  (deg `  p )
82cv 1622 . . . . . . 7  class  x
9 cdgraa 27345 . . . . . . 7  class degAA
108, 9cfv 5255 . . . . . 6  class  (degAA `  x
)
117, 10wceq 1623 . . . . 5  wff  (deg `  p )  =  (degAA `  x )
128, 5cfv 5255 . . . . . 6  class  ( p `
 x )
13 cc0 8737 . . . . . 6  class  0
1412, 13wceq 1623 . . . . 5  wff  ( p `
 x )  =  0
15 ccoe 19568 . . . . . . . 8  class coeff
165, 15cfv 5255 . . . . . . 7  class  (coeff `  p )
1710, 16cfv 5255 . . . . . 6  class  ( (coeff `  p ) `  (degAA `  x ) )
18 c1 8738 . . . . . 6  class  1
1917, 18wceq 1623 . . . . 5  wff  ( (coeff `  p ) `  (degAA `  x ) )  =  1
2011, 14, 19w3a 934 . . . 4  wff  ( (deg
`  p )  =  (degAA `  x )  /\  ( p `  x
)  =  0  /\  ( (coeff `  p
) `  (degAA `  x
) )  =  1 )
21 cq 10316 . . . . 5  class  QQ
22 cply 19566 . . . . 5  class Poly
2321, 22cfv 5255 . . . 4  class  (Poly `  QQ )
2420, 4, 23crio 6297 . . 3  class  ( iota_ p  e.  (Poly `  QQ ) ( (deg `  p )  =  (degAA `  x )  /\  (
p `  x )  =  0  /\  (
(coeff `  p ) `  (degAA `  x ) )  =  1 ) )
252, 3, 24cmpt 4077 . 2  class  ( x  e.  AA  |->  ( iota_ p  e.  (Poly `  QQ ) ( (deg `  p )  =  (degAA `  x )  /\  (
p `  x )  =  0  /\  (
(coeff `  p ) `  (degAA `  x ) )  =  1 ) ) )
261, 25wceq 1623 1  wff minPolyAA  =  ( x  e.  AA  |->  (
iota_ p  e.  (Poly `  QQ ) ( (deg
`  p )  =  (degAA `  x )  /\  ( p `  x
)  =  0  /\  ( (coeff `  p
) `  (degAA `  x
) )  =  1 ) ) )
Colors of variables: wff set class
This definition is referenced by:  mpaaval  27356
  Copyright terms: Public domain W3C validator