Definition df-mpaa

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)

	Ref	Expression
Assertion	df-mpaa	$$⊢{\mathrm{minPoly}}_{𝔸}=\left(x\in 𝔸⟼\left(\iota p\in \mathrm{Poly}\left(\mathbb{Q}\right)|\left(\mathrm{deg}\left(p\right)={\mathrm{deg}}_{𝔸}\left(x\right)\wedge p\left(x\right)=0\wedge \mathrm{coeff}\left(p\right)\left({\mathrm{deg}}_{𝔸}\left(x\right)\right)=1\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmpaa	$$class{\mathrm{minPoly}}_{𝔸}$$
1		vx	$$setvarx$$
2		caa	$$class𝔸$$
3		vp	$$setvarp$$
4		cply	$$class\mathrm{Poly}$$
5		cq	$$class\mathbb{Q}$$
6	5 4	cfv	$$class\mathrm{Poly}\left(\mathbb{Q}\right)$$
7		cdgr	$$class\mathrm{deg}$$
8	3	cv	$$setvarp$$
9	8 7	cfv	$$class\mathrm{deg}\left(p\right)$$
10		cdgraa	$$class{\mathrm{deg}}_{𝔸}$$
11	1	cv	$$setvarx$$
12	11 10	cfv	$$class{\mathrm{deg}}_{𝔸}\left(x\right)$$
13	9 12	wceq	$$wff\mathrm{deg}\left(p\right)={\mathrm{deg}}_{𝔸}\left(x\right)$$
14	11 8	cfv	$$classp\left(x\right)$$
15		cc0	$$class0$$
16	14 15	wceq	$$wffp\left(x\right)=0$$
17		ccoe	$$class\mathrm{coeff}$$
18	8 17	cfv	$$class\mathrm{coeff}\left(p\right)$$
19	12 18	cfv	$$class\mathrm{coeff}\left(p\right)\left({\mathrm{deg}}_{𝔸}\left(x\right)\right)$$
20		c1	$$class1$$
21	19 20	wceq	$$wff\mathrm{coeff}\left(p\right)\left({\mathrm{deg}}_{𝔸}\left(x\right)\right)=1$$
22	13 16 21	w3a	$$wff\left(\mathrm{deg}\left(p\right)={\mathrm{deg}}_{𝔸}\left(x\right)\wedge p\left(x\right)=0\wedge \mathrm{coeff}\left(p\right)\left({\mathrm{deg}}_{𝔸}\left(x\right)\right)=1\right)$$
23	22 3 6	crio	$$class\left(\iota p\in \mathrm{Poly}\left(\mathbb{Q}\right)|\left(\mathrm{deg}\left(p\right)={\mathrm{deg}}_{𝔸}\left(x\right)\wedge p\left(x\right)=0\wedge \mathrm{coeff}\left(p\right)\left({\mathrm{deg}}_{𝔸}\left(x\right)\right)=1\right)\right)$$
24	1 2 23	cmpt	$$class\left(x\in 𝔸⟼\left(\iota p\in \mathrm{Poly}\left(\mathbb{Q}\right)|\left(\mathrm{deg}\left(p\right)={\mathrm{deg}}_{𝔸}\left(x\right)\wedge p\left(x\right)=0\wedge \mathrm{coeff}\left(p\right)\left({\mathrm{deg}}_{𝔸}\left(x\right)\right)=1\right)\right)\right)$$
25	0 24	wceq	$$wff{\mathrm{minPoly}}_{𝔸}=\left(x\in 𝔸⟼\left(\iota p\in \mathrm{Poly}\left(\mathbb{Q}\right)|\left(\mathrm{deg}\left(p\right)={\mathrm{deg}}_{𝔸}\left(x\right)\wedge p\left(x\right)=0\wedge \mathrm{coeff}\left(p\right)\left({\mathrm{deg}}_{𝔸}\left(x\right)\right)=1\right)\right)\right)$$