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 
|- ( A e. AA -> ( * ` A ) e. AA )

Proof

Step Hyp Ref Expression
1 cjcl 
 |-  ( A e. CC -> ( * ` A ) e. CC )
2 1 adantr 
 |-  ( ( A e. CC /\ E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 ) -> ( * ` A ) e. CC )
3 fveq2 
 |-  ( ( f ` A ) = 0 -> ( * ` ( f ` A ) ) = ( * ` 0 ) )
4 cj0 
 |-  ( * ` 0 ) = 0
5 3 4 eqtrdi 
 |-  ( ( f ` A ) = 0 -> ( * ` ( f ` A ) ) = 0 )
6 difss 
 |-  ( ( Poly ` ZZ ) \ { 0p } ) C_ ( Poly ` ZZ )
7 zssre 
 |-  ZZ C_ RR
8 ax-resscn 
 |-  RR C_ CC
9 plyss 
 |-  ( ( ZZ C_ RR /\ RR C_ CC ) -> ( Poly ` ZZ ) C_ ( Poly ` RR ) )
10 7 8 9 mp2an 
 |-  ( Poly ` ZZ ) C_ ( Poly ` RR )
11 6 10 sstri 
 |-  ( ( Poly ` ZZ ) \ { 0p } ) C_ ( Poly ` RR )
12 11 sseli 
 |-  ( f e. ( ( Poly ` ZZ ) \ { 0p } ) -> f e. ( Poly ` RR ) )
13 id 
 |-  ( A e. CC -> A e. CC )
14 plyrecj 
 |-  ( ( f e. ( Poly ` RR ) /\ A e. CC ) -> ( * ` ( f ` A ) ) = ( f ` ( * ` A ) ) )
15 12 13 14 syl2anr 
 |-  ( ( A e. CC /\ f e. ( ( Poly ` ZZ ) \ { 0p } ) ) -> ( * ` ( f ` A ) ) = ( f ` ( * ` A ) ) )
16 15 eqeq1d 
 |-  ( ( A e. CC /\ f e. ( ( Poly ` ZZ ) \ { 0p } ) ) -> ( ( * ` ( f ` A ) ) = 0 <-> ( f ` ( * ` A ) ) = 0 ) )
17 5 16 syl5ib 
 |-  ( ( A e. CC /\ f e. ( ( Poly ` ZZ ) \ { 0p } ) ) -> ( ( f ` A ) = 0 -> ( f ` ( * ` A ) ) = 0 ) )
18 17 reximdva 
 |-  ( A e. CC -> ( E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 -> E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` ( * ` A ) ) = 0 ) )
19 18 imp 
 |-  ( ( A e. CC /\ E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 ) -> E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` ( * ` A ) ) = 0 )
20 2 19 jca 
 |-  ( ( A e. CC /\ E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 ) -> ( ( * ` A ) e. CC /\ E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` ( * ` A ) ) = 0 ) )
21 elaa 
 |-  ( A e. AA <-> ( A e. CC /\ E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 ) )
22 elaa 
 |-  ( ( * ` A ) e. AA <-> ( ( * ` A ) e. CC /\ E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` ( * ` A ) ) = 0 ) )
23 20 21 22 3imtr4i 
 |-  ( A e. AA -> ( * ` A ) e. AA )