Metamath Proof Explorer


Theorem mpaalem

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

Ref Expression
Assertion mpaalem A 𝔸 minPoly 𝔸 A Poly deg minPoly 𝔸 A = deg 𝔸 A minPoly 𝔸 A A = 0 coeff minPoly 𝔸 A deg 𝔸 A = 1

Proof

Step Hyp Ref Expression
1 mpaaval A 𝔸 minPoly 𝔸 A = ι p Poly | deg p = deg 𝔸 A p A = 0 coeff p deg 𝔸 A = 1
2 mpaaeu A 𝔸 ∃! p Poly deg p = deg 𝔸 A p A = 0 coeff p deg 𝔸 A = 1
3 riotacl2 ∃! 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 p Poly | deg p = deg 𝔸 A p A = 0 coeff p deg 𝔸 A = 1
4 2 3 syl 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
5 1 4 eqeltrd A 𝔸 minPoly 𝔸 A p Poly | deg p = deg 𝔸 A p A = 0 coeff p deg 𝔸 A = 1
6 fveqeq2 p = minPoly 𝔸 A deg p = deg 𝔸 A deg minPoly 𝔸 A = deg 𝔸 A
7 fveq1 p = minPoly 𝔸 A p A = minPoly 𝔸 A A
8 7 eqeq1d p = minPoly 𝔸 A p A = 0 minPoly 𝔸 A A = 0
9 fveq2 p = minPoly 𝔸 A coeff p = coeff minPoly 𝔸 A
10 9 fveq1d p = minPoly 𝔸 A coeff p deg 𝔸 A = coeff minPoly 𝔸 A deg 𝔸 A
11 10 eqeq1d p = minPoly 𝔸 A coeff p deg 𝔸 A = 1 coeff minPoly 𝔸 A deg 𝔸 A = 1
12 6 8 11 3anbi123d p = minPoly 𝔸 A deg p = deg 𝔸 A p A = 0 coeff p deg 𝔸 A = 1 deg minPoly 𝔸 A = deg 𝔸 A minPoly 𝔸 A A = 0 coeff minPoly 𝔸 A deg 𝔸 A = 1
13 12 elrab minPoly 𝔸 A p Poly | deg p = deg 𝔸 A p A = 0 coeff p deg 𝔸 A = 1 minPoly 𝔸 A Poly deg minPoly 𝔸 A = deg 𝔸 A minPoly 𝔸 A A = 0 coeff minPoly 𝔸 A deg 𝔸 A = 1
14 5 13 sylib A 𝔸 minPoly 𝔸 A Poly deg minPoly 𝔸 A = deg 𝔸 A minPoly 𝔸 A A = 0 coeff minPoly 𝔸 A deg 𝔸 A = 1