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	⊢ 𝔸 = ∪ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( ◡ 𝑓 “ { 0 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		caa	⊢ 𝔸
1		vf	⊢ 𝑓
2		cply	⊢ Poly
3		cz	⊢ ℤ
4	3 2	cfv	⊢ ( Poly ‘ ℤ )
5		c0p	⊢ 0𝑝
6	5	csn	⊢ { 0𝑝 }
7	4 6	cdif	⊢ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } )
8	1	cv	⊢ 𝑓
9	8	ccnv	⊢ ◡ 𝑓
10		cc0	⊢ 0
11	10	csn	⊢ { 0 }
12	9 11	cima	⊢ ( ◡ 𝑓 “ { 0 } )
13	1 7 12	ciun	⊢ ∪ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( ◡ 𝑓 “ { 0 } )
14	0 13	wceq	⊢ 𝔸 = ∪ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( ◡ 𝑓 “ { 0 } )