Metamath Proof Explorer

Theorem plyconz

Description: The composition of a nonzero and a nonconstant polynomial is a nonzero polynomial. (Contributed by SN, 30-Aug-2026)

Ref Expression
Hypotheses plyconz.f 
|- ( ph -> F e. ( Poly ` S ) )
plyconz.g 
|- ( ph -> G e. ( Poly ` S ) )
plyconz.1 
|- ( ph -> F =/= 0p )
plyconz.2 
|- ( ph -> ( deg ` G ) =/= 0 )
Assertion plyconz 
|- ( ph -> ( F o. G ) =/= 0p )

Proof

Step Hyp Ref Expression
1 plyconz.f 
 |-  ( ph -> F e. ( Poly ` S ) )
2 plyconz.g 
 |-  ( ph -> G e. ( Poly ` S ) )
3 plyconz.1 
 |-  ( ph -> F =/= 0p )
4 plyconz.2 
 |-  ( ph -> ( deg ` G ) =/= 0 )
5 2 4 rnplynfin 
 |-  ( ph -> -. ran G e. Fin )
6 eqid 
 |-  ( `' F " { 0 } ) = ( `' F " { 0 } )
7 6 fta1 
 |-  ( ( F e. ( Poly ` S ) /\ F =/= 0p ) -> ( ( `' F " { 0 } ) e. Fin /\ ( # ` ( `' F " { 0 } ) ) <_ ( deg ` F ) ) )
8 1 3 7 syl2anc 
 |-  ( ph -> ( ( `' F " { 0 } ) e. Fin /\ ( # ` ( `' F " { 0 } ) ) <_ ( deg ` F ) ) )
9 8 simpld 
 |-  ( ph -> ( `' F " { 0 } ) e. Fin )
10 9 adantr 
 |-  ( ( ph /\ ran G C_ ( `' F " { 0 } ) ) -> ( `' F " { 0 } ) e. Fin )
11 simpr 
 |-  ( ( ph /\ ran G C_ ( `' F " { 0 } ) ) -> ran G C_ ( `' F " { 0 } ) )
12 10 11 ssfid 
 |-  ( ( ph /\ ran G C_ ( `' F " { 0 } ) ) -> ran G e. Fin )
13 5 12 mtand 
 |-  ( ph -> -. ran G C_ ( `' F " { 0 } ) )
14 plyf 
 |-  ( G e. ( Poly ` S ) -> G : CC --> CC )
15 2 14 syl 
 |-  ( ph -> G : CC --> CC )
16 15 frnd 
 |-  ( ph -> ran G C_ CC )
17 16 sseld 
 |-  ( ph -> ( z e. ran G -> z e. CC ) )
18 fveqeq2 
 |-  ( y = z -> ( ( F ` y ) = 0 <-> ( F ` z ) = 0 ) )
19 18 rspcv 
 |-  ( z e. ran G -> ( A. y e. ran G ( F ` y ) = 0 -> ( F ` z ) = 0 ) )
20 19 com12 
 |-  ( A. y e. ran G ( F ` y ) = 0 -> ( z e. ran G -> ( F ` z ) = 0 ) )
21 17 20 anim12ii 
 |-  ( ( ph /\ A. y e. ran G ( F ` y ) = 0 ) -> ( z e. ran G -> ( z e. CC /\ ( F ` z ) = 0 ) ) )
22 plyf 
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )
23 1 22 syl 
 |-  ( ph -> F : CC --> CC )
24 23 ffnd 
 |-  ( ph -> F Fn CC )
25 24 adantr 
 |-  ( ( ph /\ A. y e. ran G ( F ` y ) = 0 ) -> F Fn CC )
26 fniniseg 
 |-  ( F Fn CC -> ( z e. ( `' F " { 0 } ) <-> ( z e. CC /\ ( F ` z ) = 0 ) ) )
27 25 26 syl 
 |-  ( ( ph /\ A. y e. ran G ( F ` y ) = 0 ) -> ( z e. ( `' F " { 0 } ) <-> ( z e. CC /\ ( F ` z ) = 0 ) ) )
28 21 27 sylibrd 
 |-  ( ( ph /\ A. y e. ran G ( F ` y ) = 0 ) -> ( z e. ran G -> z e. ( `' F " { 0 } ) ) )
29 28 ssrdv 
 |-  ( ( ph /\ A. y e. ran G ( F ` y ) = 0 ) -> ran G C_ ( `' F " { 0 } ) )
30 13 29 mtand 
 |-  ( ph -> -. A. y e. ran G ( F ` y ) = 0 )
31 df-ne 
 |-  ( ( F ` y ) =/= 0 <-> -. ( F ` y ) = 0 )
32 31 rexbii 
 |-  ( E. y e. ran G ( F ` y ) =/= 0 <-> E. y e. ran G -. ( F ` y ) = 0 )
33 rexnal 
 |-  ( E. y e. ran G -. ( F ` y ) = 0 <-> -. A. y e. ran G ( F ` y ) = 0 )
34 32 33 bitri 
 |-  ( E. y e. ran G ( F ` y ) =/= 0 <-> -. A. y e. ran G ( F ` y ) = 0 )
35 30 34 sylibr 
 |-  ( ph -> E. y e. ran G ( F ` y ) =/= 0 )
36 fvexd 
 |-  ( ( ph /\ x e. CC ) -> ( G ` x ) e. _V )
37 15 ffnd 
 |-  ( ph -> G Fn CC )
38 fvelrnb 
 |-  ( G Fn CC -> ( y e. ran G <-> E. x e. CC ( G ` x ) = y ) )
39 eqcom 
 |-  ( ( G ` x ) = y <-> y = ( G ` x ) )
40 39 rexbii 
 |-  ( E. x e. CC ( G ` x ) = y <-> E. x e. CC y = ( G ` x ) )
41 38 40 bitrdi 
 |-  ( G Fn CC -> ( y e. ran G <-> E. x e. CC y = ( G ` x ) ) )
42 37 41 syl 
 |-  ( ph -> ( y e. ran G <-> E. x e. CC y = ( G ` x ) ) )
43 fveq2 
 |-  ( y = ( G ` x ) -> ( F ` y ) = ( F ` ( G ` x ) ) )
44 43 neeq1d 
 |-  ( y = ( G ` x ) -> ( ( F ` y ) =/= 0 <-> ( F ` ( G ` x ) ) =/= 0 ) )
45 44 adantl 
 |-  ( ( ph /\ y = ( G ` x ) ) -> ( ( F ` y ) =/= 0 <-> ( F ` ( G ` x ) ) =/= 0 ) )
46 36 42 45 rexxfr2d 
 |-  ( ph -> ( E. y e. ran G ( F ` y ) =/= 0 <-> E. x e. CC ( F ` ( G ` x ) ) =/= 0 ) )
47 35 46 mpbid 
 |-  ( ph -> E. x e. CC ( F ` ( G ` x ) ) =/= 0 )
48 15 ffund 
 |-  ( ph -> Fun G )
49 48 adantr 
 |-  ( ( ph /\ x e. CC ) -> Fun G )
50 15 fdmd 
 |-  ( ph -> dom G = CC )
51 50 eqimsscd 
 |-  ( ph -> CC C_ dom G )
52 51 sselda 
 |-  ( ( ph /\ x e. CC ) -> x e. dom G )
53 eqid 
 |-  ( F o. G ) = ( F o. G )
54 49 52 53 fvcod 
 |-  ( ( ph /\ x e. CC ) -> ( ( F o. G ) ` x ) = ( F ` ( G ` x ) ) )
55 54 neeq1d 
 |-  ( ( ph /\ x e. CC ) -> ( ( ( F o. G ) ` x ) =/= 0 <-> ( F ` ( G ` x ) ) =/= 0 ) )
56 55 rexbidva 
 |-  ( ph -> ( E. x e. CC ( ( F o. G ) ` x ) =/= 0 <-> E. x e. CC ( F ` ( G ` x ) ) =/= 0 ) )
57 47 56 mpbird 
 |-  ( ph -> E. x e. CC ( ( F o. G ) ` x ) =/= 0 )
58 ne0p 
 |-  ( ( x e. CC /\ ( ( F o. G ) ` x ) =/= 0 ) -> ( F o. G ) =/= 0p )
59 58 rexlimiva 
 |-  ( E. x e. CC ( ( F o. G ) ` x ) =/= 0 -> ( F o. G ) =/= 0p )
60 57 59 syl 
 |-  ( ph -> ( F o. G ) =/= 0p )