Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℚ ) )
preimaaa.0 ⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ≠ 0 )
preimaaa.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
preimaaa.1 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ 𝔸 )
Assertion preimaaa ( 𝜑 → 𝐴 ∈ 𝔸 )

Proof

Step Hyp Ref Expression
1 preimaaa.f ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℚ ) )
2 preimaaa.0 ⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ≠ 0 )
3 preimaaa.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
4 preimaaa.1 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ 𝔸 )
5 elqaa ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝔸 ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ ℂ ∧ ∃ 𝑔 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑔 ‘ ( 𝐹 ‘ 𝐴 ) ) = 0 ) )
6 5 simprbi ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝔸 → ∃ 𝑔 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑔 ‘ ( 𝐹 ‘ 𝐴 ) ) = 0 )
7 4 6 syl ⊢ ( 𝜑 → ∃ 𝑔 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑔 ‘ ( 𝐹 ‘ 𝐴 ) ) = 0 )
8 fveq1 ⊢ ( 𝑓 = ( 𝑔 ∘ 𝐹 ) → ( 𝑓 ‘ 𝐴 ) = ( ( 𝑔 ∘ 𝐹 ) ‘ 𝐴 ) )
9 8 eqeq1d ⊢ ( 𝑓 = ( 𝑔 ∘ 𝐹 ) → ( ( 𝑓 ‘ 𝐴 ) = 0 ↔ ( ( 𝑔 ∘ 𝐹 ) ‘ 𝐴 ) = 0 ) )
10 eldifi ⊢ ( 𝑔 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) → 𝑔 ∈ ( Poly ‘ ℚ ) )
11 10 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ ( 𝐹 ‘ 𝐴 ) ) = 0 ) ) → 𝑔 ∈ ( Poly ‘ ℚ ) )
12 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ ( 𝐹 ‘ 𝐴 ) ) = 0 ) ) → 𝐹 ∈ ( Poly ‘ ℚ ) )
13 qaddcl ⊢ ( ( 𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ) → ( 𝑎 + 𝑏 ) ∈ ℚ )
14 13 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ ( 𝐹 ‘ 𝐴 ) ) = 0 ) ) ∧ ( 𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ) ) → ( 𝑎 + 𝑏 ) ∈ ℚ )
15 qmulcl ⊢ ( ( 𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ) → ( 𝑎 · 𝑏 ) ∈ ℚ )
16 15 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ ( 𝐹 ‘ 𝐴 ) ) = 0 ) ) ∧ ( 𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ) ) → ( 𝑎 · 𝑏 ) ∈ ℚ )
17 11 12 14 16 plyco ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ ( 𝐹 ‘ 𝐴 ) ) = 0 ) ) → ( 𝑔 ∘ 𝐹 ) ∈ ( Poly ‘ ℚ ) )
18 eldifsni ⊢ ( 𝑔 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) → 𝑔 ≠ 0𝑝 )
19 18 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ ( 𝐹 ‘ 𝐴 ) ) = 0 ) ) → 𝑔 ≠ 0𝑝 )
20 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ ( 𝐹 ‘ 𝐴 ) ) = 0 ) ) → ( deg ‘ 𝐹 ) ≠ 0 )
21 11 12 19 20 plyconz ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ ( 𝐹 ‘ 𝐴 ) ) = 0 ) ) → ( 𝑔 ∘ 𝐹 ) ≠ 0𝑝 )
22 17 21 eldifsnd ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ ( 𝐹 ‘ 𝐴 ) ) = 0 ) ) → ( 𝑔 ∘ 𝐹 ) ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) )
23 plyf ⊢ ( 𝐹 ∈ ( Poly ‘ ℚ ) → 𝐹 : ℂ ⟶ ℂ )
24 1 23 syl ⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ )
25 24 3 fvco3d ⊢ ( 𝜑 → ( ( 𝑔 ∘ 𝐹 ) ‘ 𝐴 ) = ( 𝑔 ‘ ( 𝐹 ‘ 𝐴 ) ) )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ) → ( ( 𝑔 ∘ 𝐹 ) ‘ 𝐴 ) = ( 𝑔 ‘ ( 𝐹 ‘ 𝐴 ) ) )
27 26 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ) → ( ( ( 𝑔 ∘ 𝐹 ) ‘ 𝐴 ) = 0 ↔ ( 𝑔 ‘ ( 𝐹 ‘ 𝐴 ) ) = 0 ) )
28 27 biimprd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ) → ( ( 𝑔 ‘ ( 𝐹 ‘ 𝐴 ) ) = 0 → ( ( 𝑔 ∘ 𝐹 ) ‘ 𝐴 ) = 0 ) )
29 28 impr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ ( 𝐹 ‘ 𝐴 ) ) = 0 ) ) → ( ( 𝑔 ∘ 𝐹 ) ‘ 𝐴 ) = 0 )
30 9 22 29 rspcedvdw ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ∧ ( 𝑔 ‘ ( 𝐹 ‘ 𝐴 ) ) = 0 ) ) → ∃ 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 )
31 7 30 rexlimddv ⊢ ( 𝜑 → ∃ 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 )
32 elqaa ⊢ ( 𝐴 ∈ 𝔸 ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) )
33 3 31 32 sylanbrc ⊢ ( 𝜑 → 𝐴 ∈ 𝔸 )