Metamath Proof Explorer

Theorem coeeu

Description: Uniqueness of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Assertion coeeu 
|- ( F e. ( Poly ` S ) -> E! a e. ( CC ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )

Proof

Step Hyp Ref Expression
1 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
2 1 sseli 
 |-  ( F e. ( Poly ` S ) -> F e. ( Poly ` CC ) )
3 elply2 
 |-  ( F e. ( Poly ` CC ) <-> ( CC C_ CC /\ E. n e. NN0 E. a e. ( ( CC u. { 0 } ) ^m NN0 ) ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) )
4 3 simprbi 
 |-  ( F e. ( Poly ` CC ) -> E. n e. NN0 E. a e. ( ( CC u. { 0 } ) ^m NN0 ) ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
5 rexcom 
 |-  ( E. n e. NN0 E. a e. ( ( CC u. { 0 } ) ^m NN0 ) ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) <-> E. a e. ( ( CC u. { 0 } ) ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
6 4 5 sylib 
 |-  ( F e. ( Poly ` CC ) -> E. a e. ( ( CC u. { 0 } ) ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
7 2 6 syl 
 |-  ( F e. ( Poly ` S ) -> E. a e. ( ( CC u. { 0 } ) ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
8 0cn 
 |-  0 e. CC
9 snssi 
 |-  ( 0 e. CC -> { 0 } C_ CC )
10 8 9 ax-mp 
 |-  { 0 } C_ CC
11 ssequn2 
 |-  ( { 0 } C_ CC <-> ( CC u. { 0 } ) = CC )
12 10 11 mpbi 
 |-  ( CC u. { 0 } ) = CC
13 12 oveq1i 
 |-  ( ( CC u. { 0 } ) ^m NN0 ) = ( CC ^m NN0 )
14 13 rexeqi 
 |-  ( E. a e. ( ( CC u. { 0 } ) ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) <-> E. a e. ( CC ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
15 7 14 sylib 
 |-  ( F e. ( Poly ` S ) -> E. a e. ( CC ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
16 reeanv 
 |-  ( E. n e. NN0 E. m e. NN0 ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) <-> ( E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ E. m e. NN0 ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) )
17 simp1l 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( a e. ( CC ^m NN0 ) /\ b e. ( CC ^m NN0 ) ) ) /\ ( n e. NN0 /\ m e. NN0 ) /\ ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> F e. ( Poly ` S ) )
18 simp1rl 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( a e. ( CC ^m NN0 ) /\ b e. ( CC ^m NN0 ) ) ) /\ ( n e. NN0 /\ m e. NN0 ) /\ ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> a e. ( CC ^m NN0 ) )
19 simp1rr 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( a e. ( CC ^m NN0 ) /\ b e. ( CC ^m NN0 ) ) ) /\ ( n e. NN0 /\ m e. NN0 ) /\ ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> b e. ( CC ^m NN0 ) )
20 simp2l 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( a e. ( CC ^m NN0 ) /\ b e. ( CC ^m NN0 ) ) ) /\ ( n e. NN0 /\ m e. NN0 ) /\ ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> n e. NN0 )
21 simp2r 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( a e. ( CC ^m NN0 ) /\ b e. ( CC ^m NN0 ) ) ) /\ ( n e. NN0 /\ m e. NN0 ) /\ ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> m e. NN0 )
22 simp3ll 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( a e. ( CC ^m NN0 ) /\ b e. ( CC ^m NN0 ) ) ) /\ ( n e. NN0 /\ m e. NN0 ) /\ ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } )
23 simp3rl 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( a e. ( CC ^m NN0 ) /\ b e. ( CC ^m NN0 ) ) ) /\ ( n e. NN0 /\ m e. NN0 ) /\ ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } )
24 simp3lr 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( a e. ( CC ^m NN0 ) /\ b e. ( CC ^m NN0 ) ) ) /\ ( n e. NN0 /\ m e. NN0 ) /\ ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) )
25 oveq1 
 |-  ( z = w -> ( z ^ k ) = ( w ^ k ) )
26 25 oveq2d 
 |-  ( z = w -> ( ( a ` k ) x. ( z ^ k ) ) = ( ( a ` k ) x. ( w ^ k ) ) )
27 26 sumeq2sdv 
 |-  ( z = w -> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( w ^ k ) ) )
28 fveq2 
 |-  ( k = j -> ( a ` k ) = ( a ` j ) )
29 oveq2 
 |-  ( k = j -> ( w ^ k ) = ( w ^ j ) )
30 28 29 oveq12d 
 |-  ( k = j -> ( ( a ` k ) x. ( w ^ k ) ) = ( ( a ` j ) x. ( w ^ j ) ) )
31 30 cbvsumv 
 |-  sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( w ^ k ) ) = sum_ j e. ( 0 ... n ) ( ( a ` j ) x. ( w ^ j ) )
32 27 31 eqtrdi 
 |-  ( z = w -> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) = sum_ j e. ( 0 ... n ) ( ( a ` j ) x. ( w ^ j ) ) )
33 32 cbvmptv 
 |-  ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) = ( w e. CC |-> sum_ j e. ( 0 ... n ) ( ( a ` j ) x. ( w ^ j ) ) )
34 24 33 eqtrdi 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( a e. ( CC ^m NN0 ) /\ b e. ( CC ^m NN0 ) ) ) /\ ( n e. NN0 /\ m e. NN0 ) /\ ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> F = ( w e. CC |-> sum_ j e. ( 0 ... n ) ( ( a ` j ) x. ( w ^ j ) ) ) )
35 simp3rr 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( a e. ( CC ^m NN0 ) /\ b e. ( CC ^m NN0 ) ) ) /\ ( n e. NN0 /\ m e. NN0 ) /\ ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) )
36 25 oveq2d 
 |-  ( z = w -> ( ( b ` k ) x. ( z ^ k ) ) = ( ( b ` k ) x. ( w ^ k ) ) )
37 36 sumeq2sdv 
 |-  ( z = w -> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( w ^ k ) ) )
38 fveq2 
 |-  ( k = j -> ( b ` k ) = ( b ` j ) )
39 38 29 oveq12d 
 |-  ( k = j -> ( ( b ` k ) x. ( w ^ k ) ) = ( ( b ` j ) x. ( w ^ j ) ) )
40 39 cbvsumv 
 |-  sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( w ^ k ) ) = sum_ j e. ( 0 ... m ) ( ( b ` j ) x. ( w ^ j ) )
41 37 40 eqtrdi 
 |-  ( z = w -> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) = sum_ j e. ( 0 ... m ) ( ( b ` j ) x. ( w ^ j ) ) )
42 41 cbvmptv 
 |-  ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) = ( w e. CC |-> sum_ j e. ( 0 ... m ) ( ( b ` j ) x. ( w ^ j ) ) )
43 35 42 eqtrdi 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( a e. ( CC ^m NN0 ) /\ b e. ( CC ^m NN0 ) ) ) /\ ( n e. NN0 /\ m e. NN0 ) /\ ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> F = ( w e. CC |-> sum_ j e. ( 0 ... m ) ( ( b ` j ) x. ( w ^ j ) ) ) )
44 17 18 19 20 21 22 23 34 43 coeeulem 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( a e. ( CC ^m NN0 ) /\ b e. ( CC ^m NN0 ) ) ) /\ ( n e. NN0 /\ m e. NN0 ) /\ ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> a = b )
45 44 3expia 
 |-  ( ( ( F e. ( Poly ` S ) /\ ( a e. ( CC ^m NN0 ) /\ b e. ( CC ^m NN0 ) ) ) /\ ( n e. NN0 /\ m e. NN0 ) ) -> ( ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) -> a = b ) )
46 45 rexlimdvva 
 |-  ( ( F e. ( Poly ` S ) /\ ( a e. ( CC ^m NN0 ) /\ b e. ( CC ^m NN0 ) ) ) -> ( E. n e. NN0 E. m e. NN0 ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) -> a = b ) )
47 16 46 syl5bir 
 |-  ( ( F e. ( Poly ` S ) /\ ( a e. ( CC ^m NN0 ) /\ b e. ( CC ^m NN0 ) ) ) -> ( ( E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ E. m e. NN0 ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) -> a = b ) )
48 47 ralrimivva 
 |-  ( F e. ( Poly ` S ) -> A. a e. ( CC ^m NN0 ) A. b e. ( CC ^m NN0 ) ( ( E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ E. m e. NN0 ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) -> a = b ) )
49 imaeq1 
 |-  ( a = b -> ( a " ( ZZ>= ` ( n + 1 ) ) ) = ( b " ( ZZ>= ` ( n + 1 ) ) ) )
50 49 eqeq1d 
 |-  ( a = b -> ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } <-> ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } ) )
51 fveq1 
 |-  ( a = b -> ( a ` k ) = ( b ` k ) )
52 51 oveq1d 
 |-  ( a = b -> ( ( a ` k ) x. ( z ^ k ) ) = ( ( b ` k ) x. ( z ^ k ) ) )
53 52 sumeq2sdv 
 |-  ( a = b -> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) )
54 53 mpteq2dv 
 |-  ( a = b -> ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) )
55 54 eqeq2d 
 |-  ( a = b -> ( F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) <-> F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) )
56 50 55 anbi12d 
 |-  ( a = b -> ( ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) <-> ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) )
57 56 rexbidv 
 |-  ( a = b -> ( E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) <-> E. n e. NN0 ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) )
58 fvoveq1 
 |-  ( n = m -> ( ZZ>= ` ( n + 1 ) ) = ( ZZ>= ` ( m + 1 ) ) )
59 58 imaeq2d 
 |-  ( n = m -> ( b " ( ZZ>= ` ( n + 1 ) ) ) = ( b " ( ZZ>= ` ( m + 1 ) ) ) )
60 59 eqeq1d 
 |-  ( n = m -> ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } <-> ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } ) )
61 oveq2 
 |-  ( n = m -> ( 0 ... n ) = ( 0 ... m ) )
62 61 sumeq1d 
 |-  ( n = m -> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) )
63 62 mpteq2dv 
 |-  ( n = m -> ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) )
64 63 eqeq2d 
 |-  ( n = m -> ( F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) <-> F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) )
65 60 64 anbi12d 
 |-  ( n = m -> ( ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) <-> ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) )
66 65 cbvrexvw 
 |-  ( E. n e. NN0 ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) <-> E. m e. NN0 ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) )
67 57 66 bitrdi 
 |-  ( a = b -> ( E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) <-> E. m e. NN0 ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) )
68 67 reu4 
 |-  ( E! a e. ( CC ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) <-> ( E. a e. ( CC ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ A. a e. ( CC ^m NN0 ) A. b e. ( CC ^m NN0 ) ( ( E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ E. m e. NN0 ( ( b " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) -> a = b ) ) )
69 15 48 68 sylanbrc 
 |-  ( F e. ( Poly ` S ) -> E! a e. ( CC ^m NN0 ) E. n e. NN0 ( ( a " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )