Definition df-mpaa 37713

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 = ( x e. AA |-> ( iota_ p e. (Poly ` QQ ) ( (deg ` p ) = (degAA ` x ) /\ ( p ` x ) = 0 /\ ( (coeff ` p ) ` (degAA ` x ) ) = 1 ) ) )

Distinct variable group:   x, p

Detailed syntax breakdown of Definition df-mpaa

Step	Hyp	Ref	Expression
1		cmpaa 37711	. 2 class minPolyAA
2		vx	. . 3 setvar x
3		caa 24069	. . 3 class AA
4		vp	. . . . . . . 8 setvar p
5	4	cv 1482	. . . . . . 7 class p
6		cdgr 23943	. . . . . . 7 class deg
7	5, 6	cfv 5888	. . . . . 6 class (deg ` p )
8	2	cv 1482	. . . . . . 7 class x
9		cdgraa 37710	. . . . . . 7 class degAA
10	8, 9	cfv 5888	. . . . . 6 class (degAA ` x )
11	7, 10	wceq 1483	. . . . 5 wff (deg ` p ) = (degAA ` x )
12	8, 5	cfv 5888	. . . . . 6 class ( p ` x )
13		cc0 9936	. . . . . 6 class 0
14	12, 13	wceq 1483	. . . . 5 wff ( p ` x ) = 0
15		ccoe 23942	. . . . . . . 8 class coeff
16	5, 15	cfv 5888	. . . . . . 7 class (coeff ` p )
17	10, 16	cfv 5888	. . . . . 6 class ( (coeff ` p ) ` (degAA ` x ) )
18		c1 9937	. . . . . 6 class 1
19	17, 18	wceq 1483	. . . . 5 wff ( (coeff ` p ) ` (degAA ` x ) ) = 1
20	11, 14, 19	w3a 1037	. . . 4 wff ( (deg ` p ) = (degAA ` x ) /\ ( p ` x ) = 0 /\ ( (coeff ` p ) ` (degAA ` x ) ) = 1 )
21		cq 11788	. . . . 5 class QQ
22		cply 23940	. . . . 5 class Poly
23	21, 22	cfv 5888	. . . 4 class (Poly ` QQ )
24	20, 4, 23	crio 6610	. . 3 class ( iota_ p e. (Poly ` QQ ) ( (deg ` p ) = (degAA ` x ) /\ ( p ` x ) = 0 /\ ( (coeff ` p ) ` (degAA ` x ) ) = 1 ) )
25	2, 3, 24	cmpt 4729	. 2 class ( x e. AA |-> ( iota_ p e. (Poly ` QQ ) ( (deg ` p ) = (degAA ` x ) /\ ( p ` x ) = 0 /\ ( (coeff ` p ) ` (degAA ` x ) ) = 1 ) ) )
26	1, 25	wceq 1483	1 wff minPolyAA = ( x e. AA |-> ( iota_ p e. (Poly ` QQ ) ( (deg ` p ) = (degAA ` x ) /\ ( p ` x ) = 0 /\ ( (coeff ` p ) ` (degAA ` x ) ) = 1 ) ) )

This definition is referenced by:  mpaaval  37721