Theorem mpaalem

Description: Properties of the minimal polynomial of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014)

	Ref	Expression
Assertion	mpaalem	⊢ ( 𝐴 ∈ 𝔸 → ( ( minPolyAA ‘ 𝐴 ) ∈ ( Poly ‘ ℚ ) ∧ ( ( deg ‘ ( minPolyAA ‘ 𝐴 ) ) = ( degAA ‘ 𝐴 ) ∧ ( ( minPolyAA ‘ 𝐴 ) ‘ 𝐴 ) = 0 ∧ ( ( coeff ‘ ( minPolyAA ‘ 𝐴 ) ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mpaaval	⊢ ( 𝐴 ∈ 𝔸 → ( minPolyAA ‘ 𝐴 ) = ( ℩ 𝑝 ∈ ( Poly ‘ ℚ ) ( ( deg ‘ 𝑝 ) = ( degAA ‘ 𝐴 ) ∧ ( 𝑝 ‘ 𝐴 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ) ) )
2		mpaaeu	⊢ ( 𝐴 ∈ 𝔸 → ∃! 𝑝 ∈ ( Poly ‘ ℚ ) ( ( deg ‘ 𝑝 ) = ( degAA ‘ 𝐴 ) ∧ ( 𝑝 ‘ 𝐴 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ) )
3		riotacl2	⊢ ( ∃! 𝑝 ∈ ( Poly ‘ ℚ ) ( ( deg ‘ 𝑝 ) = ( degAA ‘ 𝐴 ) ∧ ( 𝑝 ‘ 𝐴 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ) → ( ℩ 𝑝 ∈ ( Poly ‘ ℚ ) ( ( deg ‘ 𝑝 ) = ( degAA ‘ 𝐴 ) ∧ ( 𝑝 ‘ 𝐴 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ) ) ∈ { 𝑝 ∈ ( Poly ‘ ℚ ) ∣ ( ( deg ‘ 𝑝 ) = ( degAA ‘ 𝐴 ) ∧ ( 𝑝 ‘ 𝐴 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ) } )
4	2 3	syl	⊢ ( 𝐴 ∈ 𝔸 → ( ℩ 𝑝 ∈ ( Poly ‘ ℚ ) ( ( deg ‘ 𝑝 ) = ( degAA ‘ 𝐴 ) ∧ ( 𝑝 ‘ 𝐴 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ) ) ∈ { 𝑝 ∈ ( Poly ‘ ℚ ) ∣ ( ( deg ‘ 𝑝 ) = ( degAA ‘ 𝐴 ) ∧ ( 𝑝 ‘ 𝐴 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ) } )
5	1 4	eqeltrd	⊢ ( 𝐴 ∈ 𝔸 → ( minPolyAA ‘ 𝐴 ) ∈ { 𝑝 ∈ ( Poly ‘ ℚ ) ∣ ( ( deg ‘ 𝑝 ) = ( degAA ‘ 𝐴 ) ∧ ( 𝑝 ‘ 𝐴 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ) } )
6		fveqeq2	⊢ ( 𝑝 = ( minPolyAA ‘ 𝐴 ) → ( ( deg ‘ 𝑝 ) = ( degAA ‘ 𝐴 ) ↔ ( deg ‘ ( minPolyAA ‘ 𝐴 ) ) = ( degAA ‘ 𝐴 ) ) )
7		fveq1	⊢ ( 𝑝 = ( minPolyAA ‘ 𝐴 ) → ( 𝑝 ‘ 𝐴 ) = ( ( minPolyAA ‘ 𝐴 ) ‘ 𝐴 ) )
8	7	eqeq1d	⊢ ( 𝑝 = ( minPolyAA ‘ 𝐴 ) → ( ( 𝑝 ‘ 𝐴 ) = 0 ↔ ( ( minPolyAA ‘ 𝐴 ) ‘ 𝐴 ) = 0 ) )
9		fveq2	⊢ ( 𝑝 = ( minPolyAA ‘ 𝐴 ) → ( coeff ‘ 𝑝 ) = ( coeff ‘ ( minPolyAA ‘ 𝐴 ) ) )
10	9	fveq1d	⊢ ( 𝑝 = ( minPolyAA ‘ 𝐴 ) → ( ( coeff ‘ 𝑝 ) ‘ ( degAA ‘ 𝐴 ) ) = ( ( coeff ‘ ( minPolyAA ‘ 𝐴 ) ) ‘ ( degAA ‘ 𝐴 ) ) )
11	10	eqeq1d	⊢ ( 𝑝 = ( minPolyAA ‘ 𝐴 ) → ( ( ( coeff ‘ 𝑝 ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ↔ ( ( coeff ‘ ( minPolyAA ‘ 𝐴 ) ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ) )
12	6 8 11	3anbi123d	⊢ ( 𝑝 = ( minPolyAA ‘ 𝐴 ) → ( ( ( deg ‘ 𝑝 ) = ( degAA ‘ 𝐴 ) ∧ ( 𝑝 ‘ 𝐴 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ) ↔ ( ( deg ‘ ( minPolyAA ‘ 𝐴 ) ) = ( degAA ‘ 𝐴 ) ∧ ( ( minPolyAA ‘ 𝐴 ) ‘ 𝐴 ) = 0 ∧ ( ( coeff ‘ ( minPolyAA ‘ 𝐴 ) ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ) ) )
13	12	elrab	⊢ ( ( minPolyAA ‘ 𝐴 ) ∈ { 𝑝 ∈ ( Poly ‘ ℚ ) ∣ ( ( deg ‘ 𝑝 ) = ( degAA ‘ 𝐴 ) ∧ ( 𝑝 ‘ 𝐴 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ) } ↔ ( ( minPolyAA ‘ 𝐴 ) ∈ ( Poly ‘ ℚ ) ∧ ( ( deg ‘ ( minPolyAA ‘ 𝐴 ) ) = ( degAA ‘ 𝐴 ) ∧ ( ( minPolyAA ‘ 𝐴 ) ‘ 𝐴 ) = 0 ∧ ( ( coeff ‘ ( minPolyAA ‘ 𝐴 ) ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ) ) )
14	5 13	sylib	⊢ ( 𝐴 ∈ 𝔸 → ( ( minPolyAA ‘ 𝐴 ) ∈ ( Poly ‘ ℚ ) ∧ ( ( deg ‘ ( minPolyAA ‘ 𝐴 ) ) = ( degAA ‘ 𝐴 ) ∧ ( ( minPolyAA ‘ 𝐴 ) ‘ 𝐴 ) = 0 ∧ ( ( coeff ‘ ( minPolyAA ‘ 𝐴 ) ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ) ) )