Step |
Hyp |
Ref |
Expression |
1 |
|
mpaalem |
⊢ ( 𝐴 ∈ 𝔸 → ( ( minPolyAA ‘ 𝐴 ) ∈ ( Poly ‘ ℚ ) ∧ ( ( deg ‘ ( minPolyAA ‘ 𝐴 ) ) = ( degAA ‘ 𝐴 ) ∧ ( ( minPolyAA ‘ 𝐴 ) ‘ 𝐴 ) = 0 ∧ ( ( coeff ‘ ( minPolyAA ‘ 𝐴 ) ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ) ) ) |
2 |
|
simpr1 |
⊢ ( ( ( minPolyAA ‘ 𝐴 ) ∈ ( Poly ‘ ℚ ) ∧ ( ( deg ‘ ( minPolyAA ‘ 𝐴 ) ) = ( degAA ‘ 𝐴 ) ∧ ( ( minPolyAA ‘ 𝐴 ) ‘ 𝐴 ) = 0 ∧ ( ( coeff ‘ ( minPolyAA ‘ 𝐴 ) ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ) ) → ( deg ‘ ( minPolyAA ‘ 𝐴 ) ) = ( degAA ‘ 𝐴 ) ) |
3 |
1 2
|
syl |
⊢ ( 𝐴 ∈ 𝔸 → ( deg ‘ ( minPolyAA ‘ 𝐴 ) ) = ( degAA ‘ 𝐴 ) ) |