Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mpaa Structured version   Visualization version   GIF version

Definition df-mpaa 36732
 Description: Define the minimal polynomial of an algebraic number as the unique monic polynomial which achieves the minimum of degAA. (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
StepHypRef Expression
1 cmpaa 36730 . 2 class minPolyAA
2 vx . . 3 setvar 𝑥
3 caa 23873 . . 3 class 𝔸
4 vp . . . . . . . 8 setvar 𝑝
54cv 1474 . . . . . . 7 class 𝑝
6 cdgr 23747 . . . . . . 7 class deg
75, 6cfv 5804 . . . . . 6 class (deg‘𝑝)
82cv 1474 . . . . . . 7 class 𝑥
9 cdgraa 36729 . . . . . . 7 class degAA
108, 9cfv 5804 . . . . . 6 class (degAA𝑥)
117, 10wceq 1475 . . . . 5 wff (deg‘𝑝) = (degAA𝑥)
128, 5cfv 5804 . . . . . 6 class (𝑝𝑥)
13 cc0 9815 . . . . . 6 class 0
1412, 13wceq 1475 . . . . 5 wff (𝑝𝑥) = 0
15 ccoe 23746 . . . . . . . 8 class coeff
165, 15cfv 5804 . . . . . . 7 class (coeff‘𝑝)
1710, 16cfv 5804 . . . . . 6 class ((coeff‘𝑝)‘(degAA𝑥))
18 c1 9816 . . . . . 6 class 1
1917, 18wceq 1475 . . . . 5 wff ((coeff‘𝑝)‘(degAA𝑥)) = 1
2011, 14, 19w3a 1031 . . . 4 wff ((deg‘𝑝) = (degAA𝑥) ∧ (𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(degAA𝑥)) = 1)
21 cq 11664 . . . . 5 class
22 cply 23744 . . . . 5 class Poly
2321, 22cfv 5804 . . . 4 class (Poly‘ℚ)
2420, 4, 23crio 6510 . . 3 class (𝑝 ∈ (Poly‘ℚ)((deg‘𝑝) = (degAA𝑥) ∧ (𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(degAA𝑥)) = 1))
252, 3, 24cmpt 4643 . 2 class (𝑥 ∈ 𝔸 ↦ (𝑝 ∈ (Poly‘ℚ)((deg‘𝑝) = (degAA𝑥) ∧ (𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(degAA𝑥)) = 1)))
261, 25wceq 1475 1 wff minPolyAA = (𝑥 ∈ 𝔸 ↦ (𝑝 ∈ (Poly‘ℚ)((deg‘𝑝) = (degAA𝑥) ∧ (𝑝𝑥) = 0 ∧ ((coeff‘𝑝)‘(degAA𝑥)) = 1)))
 Colors of variables: wff setvar class This definition is referenced by:  mpaaval  36740
 Copyright terms: Public domain W3C validator