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 
|- ( ph -> F e. ( Poly ` QQ ) )
preimaaa.0 
|- ( ph -> ( deg ` F ) =/= 0 )
preimaaa.a 
|- ( ph -> A e. CC )
preimaaa.1 
|- ( ph -> ( F ` A ) e. AA )
Assertion preimaaa 
|- ( ph -> A e. AA )

Proof

Step Hyp Ref Expression
1 preimaaa.f 
 |-  ( ph -> F e. ( Poly ` QQ ) )
2 preimaaa.0 
 |-  ( ph -> ( deg ` F ) =/= 0 )
3 preimaaa.a 
 |-  ( ph -> A e. CC )
4 preimaaa.1 
 |-  ( ph -> ( F ` A ) e. AA )
5 elqaa 
 |-  ( ( F ` A ) e. AA <-> ( ( F ` A ) e. CC /\ E. g e. ( ( Poly ` QQ ) \ { 0p } ) ( g ` ( F ` A ) ) = 0 ) )
6 5 simprbi 
 |-  ( ( F ` A ) e. AA -> E. g e. ( ( Poly ` QQ ) \ { 0p } ) ( g ` ( F ` A ) ) = 0 )
7 4 6 syl 
 |-  ( ph -> E. g e. ( ( Poly ` QQ ) \ { 0p } ) ( g ` ( F ` A ) ) = 0 )
8 fveq1 
 |-  ( f = ( g o. F ) -> ( f ` A ) = ( ( g o. F ) ` A ) )
9 8 eqeq1d 
 |-  ( f = ( g o. F ) -> ( ( f ` A ) = 0 <-> ( ( g o. F ) ` A ) = 0 ) )
10 eldifi 
 |-  ( g e. ( ( Poly ` QQ ) \ { 0p } ) -> g e. ( Poly ` QQ ) )
11 10 ad2antrl 
 |-  ( ( ph /\ ( g e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( g ` ( F ` A ) ) = 0 ) ) -> g e. ( Poly ` QQ ) )
12 1 adantr 
 |-  ( ( ph /\ ( g e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( g ` ( F ` A ) ) = 0 ) ) -> F e. ( Poly ` QQ ) )
13 qaddcl 
 |-  ( ( a e. QQ /\ b e. QQ ) -> ( a + b ) e. QQ )
14 13 adantl 
 |-  ( ( ( ph /\ ( g e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( g ` ( F ` A ) ) = 0 ) ) /\ ( a e. QQ /\ b e. QQ ) ) -> ( a + b ) e. QQ )
15 qmulcl 
 |-  ( ( a e. QQ /\ b e. QQ ) -> ( a x. b ) e. QQ )
16 15 adantl 
 |-  ( ( ( ph /\ ( g e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( g ` ( F ` A ) ) = 0 ) ) /\ ( a e. QQ /\ b e. QQ ) ) -> ( a x. b ) e. QQ )
17 11 12 14 16 plyco 
 |-  ( ( ph /\ ( g e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( g ` ( F ` A ) ) = 0 ) ) -> ( g o. F ) e. ( Poly ` QQ ) )
18 eldifsni 
 |-  ( g e. ( ( Poly ` QQ ) \ { 0p } ) -> g =/= 0p )
19 18 ad2antrl 
 |-  ( ( ph /\ ( g e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( g ` ( F ` A ) ) = 0 ) ) -> g =/= 0p )
20 2 adantr 
 |-  ( ( ph /\ ( g e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( g ` ( F ` A ) ) = 0 ) ) -> ( deg ` F ) =/= 0 )
21 11 12 19 20 plyconz 
 |-  ( ( ph /\ ( g e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( g ` ( F ` A ) ) = 0 ) ) -> ( g o. F ) =/= 0p )
22 17 21 eldifsnd 
 |-  ( ( ph /\ ( g e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( g ` ( F ` A ) ) = 0 ) ) -> ( g o. F ) e. ( ( Poly ` QQ ) \ { 0p } ) )
23 plyf 
 |-  ( F e. ( Poly ` QQ ) -> F : CC --> CC )
24 1 23 syl 
 |-  ( ph -> F : CC --> CC )
25 24 3 fvco3d 
 |-  ( ph -> ( ( g o. F ) ` A ) = ( g ` ( F ` A ) ) )
26 25 adantr 
 |-  ( ( ph /\ g e. ( ( Poly ` QQ ) \ { 0p } ) ) -> ( ( g o. F ) ` A ) = ( g ` ( F ` A ) ) )
27 26 eqeq1d 
 |-  ( ( ph /\ g e. ( ( Poly ` QQ ) \ { 0p } ) ) -> ( ( ( g o. F ) ` A ) = 0 <-> ( g ` ( F ` A ) ) = 0 ) )
28 27 biimprd 
 |-  ( ( ph /\ g e. ( ( Poly ` QQ ) \ { 0p } ) ) -> ( ( g ` ( F ` A ) ) = 0 -> ( ( g o. F ) ` A ) = 0 ) )
29 28 impr 
 |-  ( ( ph /\ ( g e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( g ` ( F ` A ) ) = 0 ) ) -> ( ( g o. F ) ` A ) = 0 )
30 9 22 29 rspcedvdw 
 |-  ( ( ph /\ ( g e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( g ` ( F ` A ) ) = 0 ) ) -> E. f e. ( ( Poly ` QQ ) \ { 0p } ) ( f ` A ) = 0 )
31 7 30 rexlimddv 
 |-  ( ph -> E. f e. ( ( Poly ` QQ ) \ { 0p } ) ( f ` A ) = 0 )
32 elqaa 
 |-  ( A e. AA <-> ( A e. CC /\ E. f e. ( ( Poly ` QQ ) \ { 0p } ) ( f ` A ) = 0 ) )
33 3 31 32 sylanbrc 
 |-  ( ph -> A e. AA )