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