Description: Minimal polynomial is a polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | mpaacl | |- ( A e. AA -> ( minPolyAA ` A ) e. ( Poly ` QQ ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpaalem | |- ( A e. AA -> ( ( minPolyAA ` A ) e. ( Poly ` QQ ) /\ ( ( deg ` ( minPolyAA ` A ) ) = ( degAA ` A ) /\ ( ( minPolyAA ` A ) ` A ) = 0 /\ ( ( coeff ` ( minPolyAA ` A ) ) ` ( degAA ` A ) ) = 1 ) ) ) |
|
2 | 1 | simpld | |- ( A e. AA -> ( minPolyAA ` A ) e. ( Poly ` QQ ) ) |