Metamath Proof Explorer

Theorem plyeq0

Description: If a polynomial is zero at every point (or even just zero at the positive integers), then all the coefficients must be zero. This is the basis for the method of equating coefficients of equal polynomials, and ensures that df-coe is well-defined. (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Hypotheses plyeq0.1 
|- ( ph -> S C_ CC )
plyeq0.2 
|- ( ph -> N e. NN0 )
plyeq0.3 
|- ( ph -> A e. ( ( S u. { 0 } ) ^m NN0 ) )
plyeq0.4 
|- ( ph -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
plyeq0.5 
|- ( ph -> 0p = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )
Assertion plyeq0 
|- ( ph -> A = ( NN0 X. { 0 } ) )

Proof

Step Hyp Ref Expression
1 plyeq0.1 
 |-  ( ph -> S C_ CC )
2 plyeq0.2 
 |-  ( ph -> N e. NN0 )
3 plyeq0.3 
 |-  ( ph -> A e. ( ( S u. { 0 } ) ^m NN0 ) )
4 plyeq0.4 
 |-  ( ph -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
5 plyeq0.5 
 |-  ( ph -> 0p = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )
6 0cnd 
 |-  ( ph -> 0 e. CC )
7 6 snssd 
 |-  ( ph -> { 0 } C_ CC )
8 1 7 unssd 
 |-  ( ph -> ( S u. { 0 } ) C_ CC )
9 cnex 
 |-  CC e. _V
10 ssexg 
 |-  ( ( ( S u. { 0 } ) C_ CC /\ CC e. _V ) -> ( S u. { 0 } ) e. _V )
11 8 9 10 sylancl 
 |-  ( ph -> ( S u. { 0 } ) e. _V )
12 nn0ex 
 |-  NN0 e. _V
13 elmapg 
 |-  ( ( ( S u. { 0 } ) e. _V /\ NN0 e. _V ) -> ( A e. ( ( S u. { 0 } ) ^m NN0 ) <-> A : NN0 --> ( S u. { 0 } ) ) )
14 11 12 13 sylancl 
 |-  ( ph -> ( A e. ( ( S u. { 0 } ) ^m NN0 ) <-> A : NN0 --> ( S u. { 0 } ) ) )
15 3 14 mpbid 
 |-  ( ph -> A : NN0 --> ( S u. { 0 } ) )
16 15 ffnd 
 |-  ( ph -> A Fn NN0 )
17 imadmrn 
 |-  ( A " dom A ) = ran A
18 fdm 
 |-  ( A : NN0 --> ( S u. { 0 } ) -> dom A = NN0 )
19 fimacnv 
 |-  ( A : NN0 --> ( S u. { 0 } ) -> ( `' A " ( S u. { 0 } ) ) = NN0 )
20 18 19 eqtr4d 
 |-  ( A : NN0 --> ( S u. { 0 } ) -> dom A = ( `' A " ( S u. { 0 } ) ) )
21 15 20 syl 
 |-  ( ph -> dom A = ( `' A " ( S u. { 0 } ) ) )
22 simpr 
 |-  ( ( ph /\ ( `' A " ( S \ { 0 } ) ) = (/) ) -> ( `' A " ( S \ { 0 } ) ) = (/) )
23 1 adantr 
 |-  ( ( ph /\ ( `' A " ( S \ { 0 } ) ) =/= (/) ) -> S C_ CC )
24 2 adantr 
 |-  ( ( ph /\ ( `' A " ( S \ { 0 } ) ) =/= (/) ) -> N e. NN0 )
25 3 adantr 
 |-  ( ( ph /\ ( `' A " ( S \ { 0 } ) ) =/= (/) ) -> A e. ( ( S u. { 0 } ) ^m NN0 ) )
26 4 adantr 
 |-  ( ( ph /\ ( `' A " ( S \ { 0 } ) ) =/= (/) ) -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
27 5 adantr 
 |-  ( ( ph /\ ( `' A " ( S \ { 0 } ) ) =/= (/) ) -> 0p = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )
28 eqid 
 |-  sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) = sup ( ( `' A " ( S \ { 0 } ) ) , RR , < )
29 simpr 
 |-  ( ( ph /\ ( `' A " ( S \ { 0 } ) ) =/= (/) ) -> ( `' A " ( S \ { 0 } ) ) =/= (/) )
30 23 24 25 26 27 28 29 plyeq0lem 
 |-  -. ( ph /\ ( `' A " ( S \ { 0 } ) ) =/= (/) )
31 30 pm2.21i 
 |-  ( ( ph /\ ( `' A " ( S \ { 0 } ) ) =/= (/) ) -> ( `' A " ( S \ { 0 } ) ) = (/) )
32 22 31 pm2.61dane 
 |-  ( ph -> ( `' A " ( S \ { 0 } ) ) = (/) )
33 32 uneq1d 
 |-  ( ph -> ( ( `' A " ( S \ { 0 } ) ) u. ( `' A " { 0 } ) ) = ( (/) u. ( `' A " { 0 } ) ) )
34 undif1 
 |-  ( ( S \ { 0 } ) u. { 0 } ) = ( S u. { 0 } )
35 34 imaeq2i 
 |-  ( `' A " ( ( S \ { 0 } ) u. { 0 } ) ) = ( `' A " ( S u. { 0 } ) )
36 imaundi 
 |-  ( `' A " ( ( S \ { 0 } ) u. { 0 } ) ) = ( ( `' A " ( S \ { 0 } ) ) u. ( `' A " { 0 } ) )
37 35 36 eqtr3i 
 |-  ( `' A " ( S u. { 0 } ) ) = ( ( `' A " ( S \ { 0 } ) ) u. ( `' A " { 0 } ) )
38 un0 
 |-  ( ( `' A " { 0 } ) u. (/) ) = ( `' A " { 0 } )
39 uncom 
 |-  ( ( `' A " { 0 } ) u. (/) ) = ( (/) u. ( `' A " { 0 } ) )
40 38 39 eqtr3i 
 |-  ( `' A " { 0 } ) = ( (/) u. ( `' A " { 0 } ) )
41 33 37 40 3eqtr4g 
 |-  ( ph -> ( `' A " ( S u. { 0 } ) ) = ( `' A " { 0 } ) )
42 21 41 eqtrd 
 |-  ( ph -> dom A = ( `' A " { 0 } ) )
43 eqimss 
 |-  ( dom A = ( `' A " { 0 } ) -> dom A C_ ( `' A " { 0 } ) )
44 42 43 syl 
 |-  ( ph -> dom A C_ ( `' A " { 0 } ) )
45 15 ffund 
 |-  ( ph -> Fun A )
46 ssid 
 |-  dom A C_ dom A
47 funimass3 
 |-  ( ( Fun A /\ dom A C_ dom A ) -> ( ( A " dom A ) C_ { 0 } <-> dom A C_ ( `' A " { 0 } ) ) )
48 45 46 47 sylancl 
 |-  ( ph -> ( ( A " dom A ) C_ { 0 } <-> dom A C_ ( `' A " { 0 } ) ) )
49 44 48 mpbird 
 |-  ( ph -> ( A " dom A ) C_ { 0 } )
50 17 49 eqsstrrid 
 |-  ( ph -> ran A C_ { 0 } )
51 df-f 
 |-  ( A : NN0 --> { 0 } <-> ( A Fn NN0 /\ ran A C_ { 0 } ) )
52 16 50 51 sylanbrc 
 |-  ( ph -> A : NN0 --> { 0 } )
53 c0ex 
 |-  0 e. _V
54 53 fconst2 
 |-  ( A : NN0 --> { 0 } <-> A = ( NN0 X. { 0 } ) )
55 52 54 sylib 
 |-  ( ph -> A = ( NN0 X. { 0 } ) )