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

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( a = A -> ( degAA ` a ) = ( degAA ` A ) )
2 1 eqeq2d 
 |-  ( a = A -> ( ( deg ` p ) = ( degAA ` a ) <-> ( deg ` p ) = ( degAA ` A ) ) )
3 fveqeq2 
 |-  ( a = A -> ( ( p ` a ) = 0 <-> ( p ` A ) = 0 ) )
4 2fveq3 
 |-  ( a = A -> ( ( coeff ` p ) ` ( degAA ` a ) ) = ( ( coeff ` p ) ` ( degAA ` A ) ) )
5 4 eqeq1d 
 |-  ( a = A -> ( ( ( coeff ` p ) ` ( degAA ` a ) ) = 1 <-> ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) )
6 2 3 5 3anbi123d 
 |-  ( a = A -> ( ( ( deg ` p ) = ( degAA ` a ) /\ ( p ` a ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` a ) ) = 1 ) <-> ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) ) )
7 6 riotabidv 
 |-  ( a = A -> ( iota_ 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 ) ) )
8 df-mpaa 
 |-  minPolyAA = ( a e. AA |-> ( iota_ p e. ( Poly ` QQ ) ( ( deg ` p ) = ( degAA ` a ) /\ ( p ` a ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` a ) ) = 1 ) ) )
9 riotaex 
 |-  ( iota_ p e. ( Poly ` QQ ) ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) ) e. _V
10 7 8 9 fvmpt 
 |-  ( A e. AA -> ( minPolyAA ` A ) = ( iota_ p e. ( Poly ` QQ ) ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) ) )