Theorem mpaalem

Description: Properties of the minimal polynomial of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014)

	Ref	Expression
Assertion	mpaalem	$$⊢A\in 𝔸\to \left({\mathrm{minPoly}}_{𝔸}\left(A\right)\in \mathrm{Poly}\left(\mathbb{Q}\right)\wedge \left(\mathrm{deg}\left({\mathrm{minPoly}}_{𝔸}\left(A\right)\right)={\mathrm{deg}}_{𝔸}\left(A\right)\wedge {\mathrm{minPoly}}_{𝔸}\left(A\right)\left(A\right)=0\wedge \mathrm{coeff}\left({\mathrm{minPoly}}_{𝔸}\left(A\right)\right)\left({\mathrm{deg}}_{𝔸}\left(A\right)\right)=1\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mpaaval	$$⊢A\in 𝔸\to {\mathrm{minPoly}}_{𝔸}\left(A\right)=\left(\iota p\in \mathrm{Poly}\left(\mathbb{Q}\right)|\left(\mathrm{deg}\left(p\right)={\mathrm{deg}}_{𝔸}\left(A\right)\wedge p\left(A\right)=0\wedge \mathrm{coeff}\left(p\right)\left({\mathrm{deg}}_{𝔸}\left(A\right)\right)=1\right)\right)$$
2		mpaaeu	$$⊢A\in 𝔸\to \exists !p\in \mathrm{Poly}\left(\mathbb{Q}\right)\left(\mathrm{deg}\left(p\right)={\mathrm{deg}}_{𝔸}\left(A\right)\wedge p\left(A\right)=0\wedge \mathrm{coeff}\left(p\right)\left({\mathrm{deg}}_{𝔸}\left(A\right)\right)=1\right)$$
3		riotacl2	$$⊢\exists !p\in \mathrm{Poly}\left(\mathbb{Q}\right)\left(\mathrm{deg}\left(p\right)={\mathrm{deg}}_{𝔸}\left(A\right)\wedge p\left(A\right)=0\wedge \mathrm{coeff}\left(p\right)\left({\mathrm{deg}}_{𝔸}\left(A\right)\right)=1\right)\to \left(\iota p\in \mathrm{Poly}\left(\mathbb{Q}\right)|\left(\mathrm{deg}\left(p\right)={\mathrm{deg}}_{𝔸}\left(A\right)\wedge p\left(A\right)=0\wedge \mathrm{coeff}\left(p\right)\left({\mathrm{deg}}_{𝔸}\left(A\right)\right)=1\right)\right)\in \left\{p\in \mathrm{Poly}\left(\mathbb{Q}\right)|\left(\mathrm{deg}\left(p\right)={\mathrm{deg}}_{𝔸}\left(A\right)\wedge p\left(A\right)=0\wedge \mathrm{coeff}\left(p\right)\left({\mathrm{deg}}_{𝔸}\left(A\right)\right)=1\right)\right\}$$
4	2 3	syl	$$⊢A\in 𝔸\to \left(\iota p\in \mathrm{Poly}\left(\mathbb{Q}\right)|\left(\mathrm{deg}\left(p\right)={\mathrm{deg}}_{𝔸}\left(A\right)\wedge p\left(A\right)=0\wedge \mathrm{coeff}\left(p\right)\left({\mathrm{deg}}_{𝔸}\left(A\right)\right)=1\right)\right)\in \left\{p\in \mathrm{Poly}\left(\mathbb{Q}\right)|\left(\mathrm{deg}\left(p\right)={\mathrm{deg}}_{𝔸}\left(A\right)\wedge p\left(A\right)=0\wedge \mathrm{coeff}\left(p\right)\left({\mathrm{deg}}_{𝔸}\left(A\right)\right)=1\right)\right\}$$
5	1 4	eqeltrd	$$⊢A\in 𝔸\to {\mathrm{minPoly}}_{𝔸}\left(A\right)\in \left\{p\in \mathrm{Poly}\left(\mathbb{Q}\right)|\left(\mathrm{deg}\left(p\right)={\mathrm{deg}}_{𝔸}\left(A\right)\wedge p\left(A\right)=0\wedge \mathrm{coeff}\left(p\right)\left({\mathrm{deg}}_{𝔸}\left(A\right)\right)=1\right)\right\}$$
6		fveqeq2	$$⊢p={\mathrm{minPoly}}_{𝔸}\left(A\right)\to \left(\mathrm{deg}\left(p\right)={\mathrm{deg}}_{𝔸}\left(A\right)\leftrightarrow \mathrm{deg}\left({\mathrm{minPoly}}_{𝔸}\left(A\right)\right)={\mathrm{deg}}_{𝔸}\left(A\right)\right)$$
7		fveq1	$$⊢p={\mathrm{minPoly}}_{𝔸}\left(A\right)\to p\left(A\right)={\mathrm{minPoly}}_{𝔸}\left(A\right)\left(A\right)$$
8	7	eqeq1d	$$⊢p={\mathrm{minPoly}}_{𝔸}\left(A\right)\to \left(p\left(A\right)=0\leftrightarrow {\mathrm{minPoly}}_{𝔸}\left(A\right)\left(A\right)=0\right)$$
9		fveq2	$$⊢p={\mathrm{minPoly}}_{𝔸}\left(A\right)\to \mathrm{coeff}\left(p\right)=\mathrm{coeff}\left({\mathrm{minPoly}}_{𝔸}\left(A\right)\right)$$
10	9	fveq1d	$$⊢p={\mathrm{minPoly}}_{𝔸}\left(A\right)\to \mathrm{coeff}\left(p\right)\left({\mathrm{deg}}_{𝔸}\left(A\right)\right)=\mathrm{coeff}\left({\mathrm{minPoly}}_{𝔸}\left(A\right)\right)\left({\mathrm{deg}}_{𝔸}\left(A\right)\right)$$
11	10	eqeq1d	$$⊢p={\mathrm{minPoly}}_{𝔸}\left(A\right)\to \left(\mathrm{coeff}\left(p\right)\left({\mathrm{deg}}_{𝔸}\left(A\right)\right)=1\leftrightarrow \mathrm{coeff}\left({\mathrm{minPoly}}_{𝔸}\left(A\right)\right)\left({\mathrm{deg}}_{𝔸}\left(A\right)\right)=1\right)$$
12	6 8 11	3anbi123d	$$⊢p={\mathrm{minPoly}}_{𝔸}\left(A\right)\to \left(\left(\mathrm{deg}\left(p\right)={\mathrm{deg}}_{𝔸}\left(A\right)\wedge p\left(A\right)=0\wedge \mathrm{coeff}\left(p\right)\left({\mathrm{deg}}_{𝔸}\left(A\right)\right)=1\right)\leftrightarrow \left(\mathrm{deg}\left({\mathrm{minPoly}}_{𝔸}\left(A\right)\right)={\mathrm{deg}}_{𝔸}\left(A\right)\wedge {\mathrm{minPoly}}_{𝔸}\left(A\right)\left(A\right)=0\wedge \mathrm{coeff}\left({\mathrm{minPoly}}_{𝔸}\left(A\right)\right)\left({\mathrm{deg}}_{𝔸}\left(A\right)\right)=1\right)\right)$$
13	12	elrab	$$⊢{\mathrm{minPoly}}_{𝔸}\left(A\right)\in \left\{p\in \mathrm{Poly}\left(\mathbb{Q}\right)|\left(\mathrm{deg}\left(p\right)={\mathrm{deg}}_{𝔸}\left(A\right)\wedge p\left(A\right)=0\wedge \mathrm{coeff}\left(p\right)\left({\mathrm{deg}}_{𝔸}\left(A\right)\right)=1\right)\right\}\leftrightarrow \left({\mathrm{minPoly}}_{𝔸}\left(A\right)\in \mathrm{Poly}\left(\mathbb{Q}\right)\wedge \left(\mathrm{deg}\left({\mathrm{minPoly}}_{𝔸}\left(A\right)\right)={\mathrm{deg}}_{𝔸}\left(A\right)\wedge {\mathrm{minPoly}}_{𝔸}\left(A\right)\left(A\right)=0\wedge \mathrm{coeff}\left({\mathrm{minPoly}}_{𝔸}\left(A\right)\right)\left({\mathrm{deg}}_{𝔸}\left(A\right)\right)=1\right)\right)$$
14	5 13	sylib	$$⊢A\in 𝔸\to \left({\mathrm{minPoly}}_{𝔸}\left(A\right)\in \mathrm{Poly}\left(\mathbb{Q}\right)\wedge \left(\mathrm{deg}\left({\mathrm{minPoly}}_{𝔸}\left(A\right)\right)={\mathrm{deg}}_{𝔸}\left(A\right)\wedge {\mathrm{minPoly}}_{𝔸}\left(A\right)\left(A\right)=0\wedge \mathrm{coeff}\left({\mathrm{minPoly}}_{𝔸}\left(A\right)\right)\left({\mathrm{deg}}_{𝔸}\left(A\right)\right)=1\right)\right)$$