Definition df-mpaa 40884

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 40882	. 2 class minPolyAA
2		vx	. . 3 setvar 𝑥
3		caa 25379	. . 3 class 𝔸
4		vp	. . . . . . . 8 setvar 𝑝
5	4	cv 1538	. . . . . . 7 class 𝑝
6		cdgr 25253	. . . . . . 7 class deg
7	5, 6	cfv 6418	. . . . . 6 class (deg‘𝑝)
8	2	cv 1538	. . . . . . 7 class 𝑥
9		cdgraa 40881	. . . . . . 7 class degAA
10	8, 9	cfv 6418	. . . . . 6 class (degAA‘𝑥)
11	7, 10	wceq 1539	. . . . 5 wff (deg‘𝑝) = (degAA‘𝑥)
12	8, 5	cfv 6418	. . . . . 6 class (𝑝‘𝑥)
13		cc0 10802	. . . . . 6 class 0
14	12, 13	wceq 1539	. . . . 5 wff (𝑝‘𝑥) = 0
15		ccoe 25252	. . . . . . . 8 class coeff
16	5, 15	cfv 6418	. . . . . . 7 class (coeff‘𝑝)
17	10, 16	cfv 6418	. . . . . 6 class ((coeff‘𝑝)‘(degAA‘𝑥))
18		c1 10803	. . . . . 6 class 1
19	17, 18	wceq 1539	. . . . 5 wff ((coeff‘𝑝)‘(degAA‘𝑥)) = 1
20	11, 14, 19	w3a 1085	. . . 4 wff ((deg‘𝑝) = (degAA‘𝑥) ∧ (𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝑥)) = 1)
21		cq 12617	. . . . 5 class ℚ
22		cply 25250	. . . . 5 class Poly
23	21, 22	cfv 6418	. . . 4 class (Poly‘ℚ)
24	20, 4, 23	crio 7211	. . 3 class (℩𝑝 ∈ (Poly‘ℚ)((deg‘𝑝) = (degAA‘𝑥) ∧ (𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝑥)) = 1))
25	2, 3, 24	cmpt 5153	. 2 class (𝑥 ∈ 𝔸 ↦ (℩𝑝 ∈ (Poly‘ℚ)((deg‘𝑝) = (degAA‘𝑥) ∧ (𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝑥)) = 1)))
26	1, 25	wceq 1539	1 wff minPolyAA = (𝑥 ∈ 𝔸 ↦ (℩𝑝 ∈ (Poly‘ℚ)((deg‘𝑝) = (degAA‘𝑥) ∧ (𝑝‘𝑥) = 0 ∧ ((coeff‘𝑝)‘(degAA‘𝑥)) = 1)))

This definition is referenced by:  mpaaval  40892