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 e. AA -> ( ( minPolyAA ` A ) e. ( Poly ` QQ ) /\ ( ( deg ` ( minPolyAA ` A ) ) = ( degAA ` A ) /\ ( ( minPolyAA ` A ) ` A ) = 0 /\ ( ( coeff ` ( minPolyAA ` A ) ) ` ( degAA ` A ) ) = 1 ) ) )

Proof

Step Hyp Ref Expression
1 mpaaval 
 |-  ( A e. AA -> ( minPolyAA ` A ) = ( iota_ p e. ( Poly ` QQ ) ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) ) )
2 mpaaeu 
 |-  ( A e. AA -> E! p e. ( Poly ` QQ ) ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) )
3 riotacl2 
 |-  ( E! p e. ( Poly ` QQ ) ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) -> ( iota_ p e. ( Poly ` QQ ) ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) ) e. { p e. ( Poly ` QQ ) | ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) } )
4 2 3 syl 
 |-  ( A e. AA -> ( iota_ p e. ( Poly ` QQ ) ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) ) e. { p e. ( Poly ` QQ ) | ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) } )
5 1 4 eqeltrd 
 |-  ( A e. AA -> ( minPolyAA ` A ) e. { p e. ( Poly ` QQ ) | ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) } )
6 fveqeq2 
 |-  ( p = ( minPolyAA ` A ) -> ( ( deg ` p ) = ( degAA ` A ) <-> ( deg ` ( minPolyAA ` A ) ) = ( degAA ` A ) ) )
7 fveq1 
 |-  ( p = ( minPolyAA ` A ) -> ( p ` A ) = ( ( minPolyAA ` A ) ` A ) )
8 7 eqeq1d 
 |-  ( p = ( minPolyAA ` A ) -> ( ( p ` A ) = 0 <-> ( ( minPolyAA ` A ) ` A ) = 0 ) )
9 fveq2 
 |-  ( p = ( minPolyAA ` A ) -> ( coeff ` p ) = ( coeff ` ( minPolyAA ` A ) ) )
10 9 fveq1d 
 |-  ( p = ( minPolyAA ` A ) -> ( ( coeff ` p ) ` ( degAA ` A ) ) = ( ( coeff ` ( minPolyAA ` A ) ) ` ( degAA ` A ) ) )
11 10 eqeq1d 
 |-  ( p = ( minPolyAA ` A ) -> ( ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 <-> ( ( coeff ` ( minPolyAA ` A ) ) ` ( degAA ` A ) ) = 1 ) )
12 6 8 11 3anbi123d 
 |-  ( p = ( minPolyAA ` A ) -> ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) <-> ( ( deg ` ( minPolyAA ` A ) ) = ( degAA ` A ) /\ ( ( minPolyAA ` A ) ` A ) = 0 /\ ( ( coeff ` ( minPolyAA ` A ) ) ` ( degAA ` A ) ) = 1 ) ) )
13 12 elrab 
 |-  ( ( minPolyAA ` A ) e. { p e. ( Poly ` QQ ) | ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) } <-> ( ( minPolyAA ` A ) e. ( Poly ` QQ ) /\ ( ( deg ` ( minPolyAA ` A ) ) = ( degAA ` A ) /\ ( ( minPolyAA ` A ) ` A ) = 0 /\ ( ( coeff ` ( minPolyAA ` A ) ) ` ( degAA ` A ) ) = 1 ) ) )
14 5 13 sylib 
 |-  ( A e. AA -> ( ( minPolyAA ` A ) e. ( Poly ` QQ ) /\ ( ( deg ` ( minPolyAA ` A ) ) = ( degAA ` A ) /\ ( ( minPolyAA ` A ) ` A ) = 0 /\ ( ( coeff ` ( minPolyAA ` A ) ) ` ( degAA ` A ) ) = 1 ) ) )