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 ) ) )