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 minPoly 𝔸 = x 𝔸 ι p Poly | deg p = deg 𝔸 x p x = 0 coeff p deg 𝔸 x = 1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmpaa class minPoly 𝔸
1 vx setvar x
2 caa class 𝔸
3 vp setvar p
4 cply class Poly
5 cq class
6 5 4 cfv class Poly
7 cdgr class deg
8 3 cv setvar p
9 8 7 cfv class deg p
10 cdgraa class deg 𝔸
11 1 cv setvar x
12 11 10 cfv class deg 𝔸 x
13 9 12 wceq wff deg p = deg 𝔸 x
14 11 8 cfv class p x
15 cc0 class 0
16 14 15 wceq wff p x = 0
17 ccoe class coeff
18 8 17 cfv class coeff p
19 12 18 cfv class coeff p deg 𝔸 x
20 c1 class 1
21 19 20 wceq wff coeff p deg 𝔸 x = 1
22 13 16 21 w3a wff deg p = deg 𝔸 x p x = 0 coeff p deg 𝔸 x = 1
23 22 3 6 crio class ι p Poly | deg p = deg 𝔸 x p x = 0 coeff p deg 𝔸 x = 1
24 1 2 23 cmpt class x 𝔸 ι p Poly | deg p = deg 𝔸 x p x = 0 coeff p deg 𝔸 x = 1
25 0 24 wceq wff minPoly 𝔸 = x 𝔸 ι p Poly | deg p = deg 𝔸 x p x = 0 coeff p deg 𝔸 x = 1