Metamath Proof Explorer

Theorem mpaaval

Description: Value of the minimal polynomial of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014)

Ref Expression
Assertion mpaaval ⊢ A ∈ 𝔸 → minPoly 𝔸 ⁡ A = ι p ∈ Poly ⁡ ℚ | deg ⁡ p = deg 𝔸 ⁡ A ∧ p ⁡ A = 0 ∧ coeff ⁡ p ⁡ deg 𝔸 ⁡ A = 1

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ a = A → deg 𝔸 ⁡ a = deg 𝔸 ⁡ A
2 1 eqeq2d ⊢ a = A → deg ⁡ p = deg 𝔸 ⁡ a ↔ deg ⁡ p = deg 𝔸 ⁡ A
3 fveqeq2 ⊢ a = A → p ⁡ a = 0 ↔ p ⁡ A = 0
4 2fveq3 ⊢ a = A → coeff ⁡ p ⁡ deg 𝔸 ⁡ a = coeff ⁡ p ⁡ deg 𝔸 ⁡ A
5 4 eqeq1d ⊢ a = A → coeff ⁡ p ⁡ deg 𝔸 ⁡ a = 1 ↔ coeff ⁡ p ⁡ deg 𝔸 ⁡ A = 1
6 2 3 5 3anbi123d ⊢ a = A → deg ⁡ p = deg 𝔸 ⁡ a ∧ p ⁡ a = 0 ∧ coeff ⁡ p ⁡ deg 𝔸 ⁡ a = 1 ↔ deg ⁡ p = deg 𝔸 ⁡ A ∧ p ⁡ A = 0 ∧ coeff ⁡ p ⁡ deg 𝔸 ⁡ A = 1
7 6 riotabidv ⊢ a = A → ι p ∈ Poly ⁡ ℚ | deg ⁡ p = deg 𝔸 ⁡ a ∧ p ⁡ a = 0 ∧ coeff ⁡ p ⁡ deg 𝔸 ⁡ a = 1 = ι p ∈ Poly ⁡ ℚ | deg ⁡ p = deg 𝔸 ⁡ A ∧ p ⁡ A = 0 ∧ coeff ⁡ p ⁡ deg 𝔸 ⁡ A = 1
8 df-mpaa ⊢ minPoly 𝔸 = a ∈ 𝔸 ⟼ ι p ∈ Poly ⁡ ℚ | deg ⁡ p = deg 𝔸 ⁡ a ∧ p ⁡ a = 0 ∧ coeff ⁡ p ⁡ deg 𝔸 ⁡ a = 1
9 riotaex ⊢ ι p ∈ Poly ⁡ ℚ | deg ⁡ p = deg 𝔸 ⁡ A ∧ p ⁡ A = 0 ∧ coeff ⁡ p ⁡ deg 𝔸 ⁡ A = 1 ∈ V
10 7 8 9 fvmpt ⊢ A ∈ 𝔸 → minPoly 𝔸 ⁡ A = ι p ∈ Poly ⁡ ℚ | deg ⁡ p = deg 𝔸 ⁡ A ∧ p ⁡ A = 0 ∧ coeff ⁡ p ⁡ deg 𝔸 ⁡ A = 1