Theorem preimaaa

Description: An element of the preimage of the algebraic numbers by a nonconstant polynomial is an algebraic number. (Contributed by SN, 30-Aug-2026)

	Ref	Expression
Hypotheses	preimaaa.f	$$⊢\phi \to F\in \mathrm{Poly}\left(\mathbb{Q}\right)$$
	preimaaa.0	$$⊢\phi \to \mathrm{deg}\left(F\right)\ne 0$$
	preimaaa.a	$$⊢\phi \to A\in ℂ$$
	preimaaa.1	$$⊢\phi \to F\left(A\right)\in 𝔸$$
Assertion	preimaaa	$$⊢\phi \to A\in 𝔸$$

Proof

Step	Hyp	Ref	Expression
1		preimaaa.f	$$⊢\phi \to F\in \mathrm{Poly}\left(\mathbb{Q}\right)$$
2		preimaaa.0	$$⊢\phi \to \mathrm{deg}\left(F\right)\ne 0$$
3		preimaaa.a	$$⊢\phi \to A\in ℂ$$
4		preimaaa.1	$$⊢\phi \to F\left(A\right)\in 𝔸$$
5		elqaa	$$⊢F\left(A\right)\in 𝔸\leftrightarrow \left(F\left(A\right)\in ℂ\wedge \exists g\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)g\left(F\left(A\right)\right)=0\right)$$
6	5	simprbi	$$⊢F\left(A\right)\in 𝔸\to \exists g\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)g\left(F\left(A\right)\right)=0$$
7	4 6	syl	$$⊢\phi \to \exists g\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)g\left(F\left(A\right)\right)=0$$
8		fveq1	$$⊢f=g\circ F\to f\left(A\right)=\left(g\circ F\right)\left(A\right)$$
9	8	eqeq1d	$$⊢f=g\circ F\to \left(f\left(A\right)=0\leftrightarrow \left(g\circ F\right)\left(A\right)=0\right)$$
10		eldifi	$$⊢g\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\to g\in \mathrm{Poly}\left(\mathbb{Q}\right)$$
11	10	ad2antrl	$$⊢\left(\phi \wedge \left(g\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\wedge g\left(F\left(A\right)\right)=0\right)\right)\to g\in \mathrm{Poly}\left(\mathbb{Q}\right)$$
12	1	adantr	$$⊢\left(\phi \wedge \left(g\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\wedge g\left(F\left(A\right)\right)=0\right)\right)\to F\in \mathrm{Poly}\left(\mathbb{Q}\right)$$
13		qaddcl	$$⊢\left(a\in \mathbb{Q}\wedge b\in \mathbb{Q}\right)\to a+b\in \mathbb{Q}$$
14	13	adantl	$$⊢\left(\left(\phi \wedge \left(g\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\wedge g\left(F\left(A\right)\right)=0\right)\right)\wedge \left(a\in \mathbb{Q}\wedge b\in \mathbb{Q}\right)\right)\to a+b\in \mathbb{Q}$$
15		qmulcl	$$⊢\left(a\in \mathbb{Q}\wedge b\in \mathbb{Q}\right)\to ab\in \mathbb{Q}$$
16	15	adantl	$$⊢\left(\left(\phi \wedge \left(g\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\wedge g\left(F\left(A\right)\right)=0\right)\right)\wedge \left(a\in \mathbb{Q}\wedge b\in \mathbb{Q}\right)\right)\to ab\in \mathbb{Q}$$
17	11 12 14 16	plyco	$$⊢\left(\phi \wedge \left(g\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\wedge g\left(F\left(A\right)\right)=0\right)\right)\to g\circ F\in \mathrm{Poly}\left(\mathbb{Q}\right)$$
18		eldifsni	$$⊢g\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\to g\ne 0_{𝑝}$$
19	18	ad2antrl	$$⊢\left(\phi \wedge \left(g\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\wedge g\left(F\left(A\right)\right)=0\right)\right)\to g\ne 0_{𝑝}$$
20	2	adantr	$$⊢\left(\phi \wedge \left(g\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\wedge g\left(F\left(A\right)\right)=0\right)\right)\to \mathrm{deg}\left(F\right)\ne 0$$
21	11 12 19 20	plyconz	$$⊢\left(\phi \wedge \left(g\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\wedge g\left(F\left(A\right)\right)=0\right)\right)\to g\circ F\ne 0_{𝑝}$$
22	17 21	eldifsnd	$$⊢\left(\phi \wedge \left(g\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\wedge g\left(F\left(A\right)\right)=0\right)\right)\to g\circ F\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)$$
23		plyf	$$⊢F\in \mathrm{Poly}\left(\mathbb{Q}\right)\to F:ℂ⟶ℂ$$
24	1 23	syl	$$⊢\phi \to F:ℂ⟶ℂ$$
25	24 3	fvco3d	$$⊢\phi \to \left(g\circ F\right)\left(A\right)=g\left(F\left(A\right)\right)$$
26	25	adantr	$$⊢\left(\phi \wedge g\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\right)\to \left(g\circ F\right)\left(A\right)=g\left(F\left(A\right)\right)$$
27	26	eqeq1d	$$⊢\left(\phi \wedge g\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\right)\to \left(\left(g\circ F\right)\left(A\right)=0\leftrightarrow g\left(F\left(A\right)\right)=0\right)$$
28	27	biimprd	$$⊢\left(\phi \wedge g\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\right)\to \left(g\left(F\left(A\right)\right)=0\to \left(g\circ F\right)\left(A\right)=0\right)$$
29	28	impr	$$⊢\left(\phi \wedge \left(g\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\wedge g\left(F\left(A\right)\right)=0\right)\right)\to \left(g\circ F\right)\left(A\right)=0$$
30	9 22 29	rspcedvdw	$$⊢\left(\phi \wedge \left(g\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\wedge g\left(F\left(A\right)\right)=0\right)\right)\to \exists f\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)f\left(A\right)=0$$
31	7 30	rexlimddv	$$⊢\phi \to \exists f\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)f\left(A\right)=0$$
32		elqaa	$$⊢A\in 𝔸\leftrightarrow \left(A\in ℂ\wedge \exists f\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)f\left(A\right)=0\right)$$
33	3 31 32	sylanbrc	$$⊢\phi \to A\in 𝔸$$