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	imbitrid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑓 ∈ ( ( 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	⊢ ( 𝐴 ∈ 𝔸 → ( ∗ ‘ 𝐴 ) ∈ 𝔸 )