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=ιpPoly|degp=deg𝔸ApA=0coeffpdeg𝔸A=1

Proof

Step Hyp Ref Expression
1 fveq2 a=Adeg𝔸a=deg𝔸A
2 1 eqeq2d a=Adegp=deg𝔸adegp=deg𝔸A
3 fveqeq2 a=Apa=0pA=0
4 2fveq3 a=Acoeffpdeg𝔸a=coeffpdeg𝔸A
5 4 eqeq1d a=Acoeffpdeg𝔸a=1coeffpdeg𝔸A=1
6 2 3 5 3anbi123d a=Adegp=deg𝔸apa=0coeffpdeg𝔸a=1degp=deg𝔸ApA=0coeffpdeg𝔸A=1
7 6 riotabidv a=AιpPoly|degp=deg𝔸apa=0coeffpdeg𝔸a=1=ιpPoly|degp=deg𝔸ApA=0coeffpdeg𝔸A=1
8 df-mpaa minPoly𝔸=a𝔸ιpPoly|degp=deg𝔸apa=0coeffpdeg𝔸a=1
9 riotaex ιpPoly|degp=deg𝔸ApA=0coeffpdeg𝔸A=1V
10 7 8 9 fvmpt A𝔸minPoly𝔸A=ιpPoly|degp=deg𝔸ApA=0coeffpdeg𝔸A=1