Description: Minimal polynomial is monic. (Contributed by Stefan O'Rear, 25-Nov-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | mpaamn | |- ( A e. AA -> ( ( coeff ` ( minPolyAA ` A ) ) ` ( degAA ` A ) ) = 1 ) |
| 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 | simpr3 | |- ( ( ( minPolyAA ` A ) e. ( Poly ` QQ ) /\ ( ( deg ` ( minPolyAA ` A ) ) = ( degAA ` A ) /\ ( ( minPolyAA ` A ) ` A ) = 0 /\ ( ( coeff ` ( minPolyAA ` A ) ) ` ( degAA ` A ) ) = 1 ) ) -> ( ( coeff ` ( minPolyAA ` A ) ) ` ( degAA ` A ) ) = 1 ) |
|
| 3 | 1 2 | syl | |- ( A e. AA -> ( ( coeff ` ( minPolyAA ` A ) ) ` ( degAA ` A ) ) = 1 ) |