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 ( 𝐴 ∈ 𝔸 → ( minPolyAA ‘ 𝐴 ) = ( 𝑝 ∈ ( Poly ‘ ℚ ) ( ( deg ‘ 𝑝 ) = ( degAA𝐴 ) ∧ ( 𝑝𝐴 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA𝐴 ) ) = 1 ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 ( 𝑎 = 𝐴 → ( degAA𝑎 ) = ( degAA𝐴 ) )
2 1 eqeq2d ( 𝑎 = 𝐴 → ( ( deg ‘ 𝑝 ) = ( degAA𝑎 ) ↔ ( deg ‘ 𝑝 ) = ( degAA𝐴 ) ) )
3 fveqeq2 ( 𝑎 = 𝐴 → ( ( 𝑝𝑎 ) = 0 ↔ ( 𝑝𝐴 ) = 0 ) )
4 2fveq3 ( 𝑎 = 𝐴 → ( ( coeff ‘ 𝑝 ) ‘ ( degAA𝑎 ) ) = ( ( coeff ‘ 𝑝 ) ‘ ( degAA𝐴 ) ) )
5 4 eqeq1d ( 𝑎 = 𝐴 → ( ( ( coeff ‘ 𝑝 ) ‘ ( degAA𝑎 ) ) = 1 ↔ ( ( coeff ‘ 𝑝 ) ‘ ( degAA𝐴 ) ) = 1 ) )
6 2 3 5 3anbi123d ( 𝑎 = 𝐴 → ( ( ( deg ‘ 𝑝 ) = ( degAA𝑎 ) ∧ ( 𝑝𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA𝑎 ) ) = 1 ) ↔ ( ( deg ‘ 𝑝 ) = ( degAA𝐴 ) ∧ ( 𝑝𝐴 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA𝐴 ) ) = 1 ) ) )
7 6 riotabidv ( 𝑎 = 𝐴 → ( 𝑝 ∈ ( Poly ‘ ℚ ) ( ( deg ‘ 𝑝 ) = ( degAA𝑎 ) ∧ ( 𝑝𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA𝑎 ) ) = 1 ) ) = ( 𝑝 ∈ ( Poly ‘ ℚ ) ( ( deg ‘ 𝑝 ) = ( degAA𝐴 ) ∧ ( 𝑝𝐴 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA𝐴 ) ) = 1 ) ) )
8 df-mpaa minPolyAA = ( 𝑎 ∈ 𝔸 ↦ ( 𝑝 ∈ ( Poly ‘ ℚ ) ( ( deg ‘ 𝑝 ) = ( degAA𝑎 ) ∧ ( 𝑝𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA𝑎 ) ) = 1 ) ) )
9 riotaex ( 𝑝 ∈ ( Poly ‘ ℚ ) ( ( deg ‘ 𝑝 ) = ( degAA𝐴 ) ∧ ( 𝑝𝐴 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA𝐴 ) ) = 1 ) ) ∈ V
10 7 8 9 fvmpt ( 𝐴 ∈ 𝔸 → ( minPolyAA ‘ 𝐴 ) = ( 𝑝 ∈ ( Poly ‘ ℚ ) ( ( deg ‘ 𝑝 ) = ( degAA𝐴 ) ∧ ( 𝑝𝐴 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA𝐴 ) ) = 1 ) ) )