Metamath Proof Explorer

Definition df-mpaa

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)

Ref Expression
Assertion df-mpaa 
|- minPolyAA = ( x e. AA |-> ( iota_ p e. ( Poly ` QQ ) ( ( deg ` p ) = ( degAA ` x ) /\ ( p ` x ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` x ) ) = 1 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmpaa 
 |-  minPolyAA
1 vx 
 |-  x
2 caa 
 |-  AA
3 vp 
 |-  p
4 cply 
 |-  Poly
5 cq 
 |-  QQ
6 5 4 cfv 
 |-  ( Poly ` QQ )
7 cdgr 
 |-  deg
8 3 cv 
 |-  p
9 8 7 cfv 
 |-  ( deg ` p )
10 cdgraa 
 |-  degAA
11 1 cv 
 |-  x
12 11 10 cfv 
 |-  ( degAA ` x )
13 9 12 wceq 
 |-  ( deg ` p ) = ( degAA ` x )
14 11 8 cfv 
 |-  ( p ` x )
15 cc0 
 |-  0
16 14 15 wceq 
 |-  ( p ` x ) = 0
17 ccoe 
 |-  coeff
18 8 17 cfv 
 |-  ( coeff ` p )
19 12 18 cfv 
 |-  ( ( coeff ` p ) ` ( degAA ` x ) )
20 c1 
 |-  1
21 19 20 wceq 
 |-  ( ( coeff ` p ) ` ( degAA ` x ) ) = 1
22 13 16 21 w3a 
 |-  ( ( deg ` p ) = ( degAA ` x ) /\ ( p ` x ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` x ) ) = 1 )
23 22 3 6 crio 
 |-  ( iota_ p e. ( Poly ` QQ ) ( ( deg ` p ) = ( degAA ` x ) /\ ( p ` x ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` x ) ) = 1 ) )
24 1 2 23 cmpt 
 |-  ( x e. AA |-> ( iota_ p e. ( Poly ` QQ ) ( ( deg ` p ) = ( degAA ` x ) /\ ( p ` x ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` x ) ) = 1 ) ) )
25 0 24 wceq 
 |-  minPolyAA = ( x e. AA |-> ( iota_ p e. ( Poly ` QQ ) ( ( deg ` p ) = ( degAA ` x ) /\ ( p ` x ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` x ) ) = 1 ) ) )