Definition df-mpaa 41875

Description: Define the minimal polynomial of an algebraic number as the unique monic polynomial which achieves the minimum of deg_AA. (Contributed by Stefan O'Rear, 25-Nov-2014.)

Assertion

Ref	Expression
df-mpaa	⊢ minPolyAA = (𝑥 ∈ 𝔸 ↦ (℩𝑝 ∈ (Poly‘ℚ)((deg‘𝑝) = (degAA‘𝑥) ∧ (𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝑥)) = 1)))

Distinct variable group:   𝑥,𝑝

Detailed syntax breakdown of Definition df-mpaa

Step	Hyp	Ref	Expression
1		cmpaa 41873	. 2 class minPolyAA
2		vx	. . 3 setvar 𝑥
3		caa 25826	. . 3 class 𝔸
4		vp	. . . . . . . 8 setvar 𝑝
5	4	cv 1540	. . . . . . 7 class 𝑝
6		cdgr 25700	. . . . . . 7 class deg
7	5, 6	cfv 6543	. . . . . 6 class (deg‘𝑝)
8	2	cv 1540	. . . . . . 7 class 𝑥
9		cdgraa 41872	. . . . . . 7 class degAA
10	8, 9	cfv 6543	. . . . . 6 class (degAA‘𝑥)
11	7, 10	wceq 1541	. . . . 5 wff (deg‘𝑝) = (degAA‘𝑥)
12	8, 5	cfv 6543	. . . . . 6 class (𝑝‘𝑥)
13		cc0 11109	. . . . . 6 class 0
14	12, 13	wceq 1541	. . . . 5 wff (𝑝‘𝑥) = 0
15		ccoe 25699	. . . . . . . 8 class coeff
16	5, 15	cfv 6543	. . . . . . 7 class (coeff‘𝑝)
17	10, 16	cfv 6543	. . . . . 6 class ((coeff‘𝑝)‘(degAA‘𝑥))
18		c1 11110	. . . . . 6 class 1
19	17, 18	wceq 1541	. . . . 5 wff ((coeff‘𝑝)‘(degAA‘𝑥)) = 1
20	11, 14, 19	w3a 1087	. . . 4 wff ((deg‘𝑝) = (degAA‘𝑥) ∧ (𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝑥)) = 1)
21		cq 12931	. . . . 5 class ℚ
22		cply 25697	. . . . 5 class Poly
23	21, 22	cfv 6543	. . . 4 class (Poly‘ℚ)
24	20, 4, 23	crio 7363	. . 3 class (℩𝑝 ∈ (Poly‘ℚ)((deg‘𝑝) = (degAA‘𝑥) ∧ (𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝑥)) = 1))
25	2, 3, 24	cmpt 5231	. 2 class (𝑥 ∈ 𝔸 ↦ (℩𝑝 ∈ (Poly‘ℚ)((deg‘𝑝) = (degAA‘𝑥) ∧ (𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝑥)) = 1)))
26	1, 25	wceq 1541	1 wff minPolyAA = (𝑥 ∈ 𝔸 ↦ (℩𝑝 ∈ (Poly‘ℚ)((deg‘𝑝) = (degAA‘𝑥) ∧ (𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝑥)) = 1)))

This definition is referenced by:  mpaaval  41883