Metamath Proof Explorer


Theorem aacjcl

Description: The conjugate of an algebraic number is algebraic. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Assertion aacjcl ( 𝐴 ∈ 𝔸 → ( ∗ ‘ 𝐴 ) ∈ 𝔸 )

Proof

Step Hyp Ref Expression
1 cjcl ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) ∈ ℂ )
2 1 adantr ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓𝐴 ) = 0 ) → ( ∗ ‘ 𝐴 ) ∈ ℂ )
3 fveq2 ( ( 𝑓𝐴 ) = 0 → ( ∗ ‘ ( 𝑓𝐴 ) ) = ( ∗ ‘ 0 ) )
4 cj0 ( ∗ ‘ 0 ) = 0
5 3 4 eqtrdi ( ( 𝑓𝐴 ) = 0 → ( ∗ ‘ ( 𝑓𝐴 ) ) = 0 )
6 difss ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ⊆ ( Poly ‘ ℤ )
7 zssre ℤ ⊆ ℝ
8 ax-resscn ℝ ⊆ ℂ
9 plyss ( ( ℤ ⊆ ℝ ∧ ℝ ⊆ ℂ ) → ( Poly ‘ ℤ ) ⊆ ( Poly ‘ ℝ ) )
10 7 8 9 mp2an ( Poly ‘ ℤ ) ⊆ ( Poly ‘ ℝ )
11 6 10 sstri ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ⊆ ( Poly ‘ ℝ )
12 11 sseli ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) → 𝑓 ∈ ( Poly ‘ ℝ ) )
13 id ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
14 plyrecj ( ( 𝑓 ∈ ( Poly ‘ ℝ ) ∧ 𝐴 ∈ ℂ ) → ( ∗ ‘ ( 𝑓𝐴 ) ) = ( 𝑓 ‘ ( ∗ ‘ 𝐴 ) ) )
15 12 13 14 syl2anr ( ( 𝐴 ∈ ℂ ∧ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ) → ( ∗ ‘ ( 𝑓𝐴 ) ) = ( 𝑓 ‘ ( ∗ ‘ 𝐴 ) ) )
16 15 eqeq1d ( ( 𝐴 ∈ ℂ ∧ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ) → ( ( ∗ ‘ ( 𝑓𝐴 ) ) = 0 ↔ ( 𝑓 ‘ ( ∗ ‘ 𝐴 ) ) = 0 ) )
17 5 16 syl5ib ( ( 𝐴 ∈ ℂ ∧ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ) → ( ( 𝑓𝐴 ) = 0 → ( 𝑓 ‘ ( ∗ ‘ 𝐴 ) ) = 0 ) )
18 17 reximdva ( 𝐴 ∈ ℂ → ( ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓𝐴 ) = 0 → ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ ( ∗ ‘ 𝐴 ) ) = 0 ) )
19 18 imp ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓𝐴 ) = 0 ) → ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ ( ∗ ‘ 𝐴 ) ) = 0 )
20 2 19 jca ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓𝐴 ) = 0 ) → ( ( ∗ ‘ 𝐴 ) ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ ( ∗ ‘ 𝐴 ) ) = 0 ) )
21 elaa ( 𝐴 ∈ 𝔸 ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓𝐴 ) = 0 ) )
22 elaa ( ( ∗ ‘ 𝐴 ) ∈ 𝔸 ↔ ( ( ∗ ‘ 𝐴 ) ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ ( ∗ ‘ 𝐴 ) ) = 0 ) )
23 20 21 22 3imtr4i ( 𝐴 ∈ 𝔸 → ( ∗ ‘ 𝐴 ) ∈ 𝔸 )