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