Users' Mathboxes 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 41513
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 41511 . 2 class minPolyAA
2 vx . . 3 setvar π‘₯
3 caa 25690 . . 3 class 𝔸
4 vp . . . . . . . 8 setvar 𝑝
54cv 1541 . . . . . . 7 class 𝑝
6 cdgr 25564 . . . . . . 7 class deg
75, 6cfv 6497 . . . . . 6 class (degβ€˜π‘)
82cv 1541 . . . . . . 7 class π‘₯
9 cdgraa 41510 . . . . . . 7 class degAA
108, 9cfv 6497 . . . . . 6 class (degAAβ€˜π‘₯)
117, 10wceq 1542 . . . . 5 wff (degβ€˜π‘) = (degAAβ€˜π‘₯)
128, 5cfv 6497 . . . . . 6 class (π‘β€˜π‘₯)
13 cc0 11056 . . . . . 6 class 0
1412, 13wceq 1542 . . . . 5 wff (π‘β€˜π‘₯) = 0
15 ccoe 25563 . . . . . . . 8 class coeff
165, 15cfv 6497 . . . . . . 7 class (coeffβ€˜π‘)
1710, 16cfv 6497 . . . . . 6 class ((coeffβ€˜π‘)β€˜(degAAβ€˜π‘₯))
18 c1 11057 . . . . . 6 class 1
1917, 18wceq 1542 . . . . 5 wff ((coeffβ€˜π‘)β€˜(degAAβ€˜π‘₯)) = 1
2011, 14, 19w3a 1088 . . . 4 wff ((degβ€˜π‘) = (degAAβ€˜π‘₯) ∧ (π‘β€˜π‘₯) = 0 ∧ ((coeffβ€˜π‘)β€˜(degAAβ€˜π‘₯)) = 1)
21 cq 12878 . . . . 5 class β„š
22 cply 25561 . . . . 5 class Poly
2321, 22cfv 6497 . . . 4 class (Polyβ€˜β„š)
2420, 4, 23crio 7313 . . 3 class (℩𝑝 ∈ (Polyβ€˜β„š)((degβ€˜π‘) = (degAAβ€˜π‘₯) ∧ (π‘β€˜π‘₯) = 0 ∧ ((coeffβ€˜π‘)β€˜(degAAβ€˜π‘₯)) = 1))
252, 3, 24cmpt 5189 . 2 class (π‘₯ ∈ 𝔸 ↦ (℩𝑝 ∈ (Polyβ€˜β„š)((degβ€˜π‘) = (degAAβ€˜π‘₯) ∧ (π‘β€˜π‘₯) = 0 ∧ ((coeffβ€˜π‘)β€˜(degAAβ€˜π‘₯)) = 1)))
261, 25wceq 1542 1 wff minPolyAA = (π‘₯ ∈ 𝔸 ↦ (℩𝑝 ∈ (Polyβ€˜β„š)((degβ€˜π‘) = (degAAβ€˜π‘₯) ∧ (π‘β€˜π‘₯) = 0 ∧ ((coeffβ€˜π‘)β€˜(degAAβ€˜π‘₯)) = 1)))
Colors of variables: wff setvar class
This definition is referenced by:  mpaaval  41521
  Copyright terms: Public domain W3C validator