Definition df-aa

Description: Define the set of algebraic numbers. An algebraic number is a root of a nonzero polynomial over the integers. Here we construct it as the union of all kernels (preimages of { 0 } ) of all polynomials in ( PolyZZ ) , except the zero polynomial 0p . (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Assertion	df-aa	$$⊢𝔸=\bigcup _{f\in \mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}}{f}^{-1}\left[\left\{0\right\}\right]$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		caa	$$class𝔸$$
1		vf	$$setvarf$$
2		cply	$$class\mathrm{Poly}$$
3		cz	$$class\mathbb{Z}$$
4	3 2	cfv	$$class\mathrm{Poly}\left(\mathbb{Z}\right)$$
5		c0p	$$class{0}_{𝑝}$$
6	5	csn	$$class\left\{0_{𝑝}\right\}$$
7	4 6	cdif	$$class\left(\mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}\right)$$
8	1	cv	$$setvarf$$
9	8	ccnv	$$class{f}^{-1}$$
10		cc0	$$class0$$
11	10	csn	$$class\left\{0\right\}$$
12	9 11	cima	$$class{f}^{-1}\left[\left\{0\right\}\right]$$
13	1 7 12	ciun	$$class\bigcup _{f\in \mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}}{f}^{-1}\left[\left\{0\right\}\right]$$
14	0 13	wceq	$$wff𝔸=\bigcup _{f\in \mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}}{f}^{-1}\left[\left\{0\right\}\right]$$