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 ( 𝜑𝑆 ⊆ ℂ )
plyeq0.2 ( 𝜑𝑁 ∈ ℕ0 )
plyeq0.3 ( 𝜑𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) )
plyeq0.4 ( 𝜑 → ( 𝐴 “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
plyeq0.5 ( 𝜑 → 0𝑝 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ) )
Assertion plyeq0 ( 𝜑𝐴 = ( ℕ0 × { 0 } ) )

Proof

Step Hyp Ref Expression
1 plyeq0.1 ( 𝜑𝑆 ⊆ ℂ )
2 plyeq0.2 ( 𝜑𝑁 ∈ ℕ0 )
3 plyeq0.3 ( 𝜑𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) )
4 plyeq0.4 ( 𝜑 → ( 𝐴 “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
5 plyeq0.5 ( 𝜑 → 0𝑝 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ) )
6 0cnd ( 𝜑 → 0 ∈ ℂ )
7 6 snssd ( 𝜑 → { 0 } ⊆ ℂ )
8 1 7 unssd ( 𝜑 → ( 𝑆 ∪ { 0 } ) ⊆ ℂ )
9 cnex ℂ ∈ V
10 ssexg ( ( ( 𝑆 ∪ { 0 } ) ⊆ ℂ ∧ ℂ ∈ V ) → ( 𝑆 ∪ { 0 } ) ∈ V )
11 8 9 10 sylancl ( 𝜑 → ( 𝑆 ∪ { 0 } ) ∈ V )
12 nn0ex 0 ∈ V
13 elmapg ( ( ( 𝑆 ∪ { 0 } ) ∈ V ∧ ℕ0 ∈ V ) → ( 𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ↔ 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
14 11 12 13 sylancl ( 𝜑 → ( 𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) ↔ 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
15 3 14 mpbid ( 𝜑𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
16 15 ffnd ( 𝜑𝐴 Fn ℕ0 )
17 imadmrn ( 𝐴 “ dom 𝐴 ) = ran 𝐴
18 fdm ( 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) → dom 𝐴 = ℕ0 )
19 fimacnv ( 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) → ( 𝐴 “ ( 𝑆 ∪ { 0 } ) ) = ℕ0 )
20 18 19 eqtr4d ( 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) → dom 𝐴 = ( 𝐴 “ ( 𝑆 ∪ { 0 } ) ) )
21 15 20 syl ( 𝜑 → dom 𝐴 = ( 𝐴 “ ( 𝑆 ∪ { 0 } ) ) )
22 simpr ( ( 𝜑 ∧ ( 𝐴 “ ( 𝑆 ∖ { 0 } ) ) = ∅ ) → ( 𝐴 “ ( 𝑆 ∖ { 0 } ) ) = ∅ )
23 1 adantr ( ( 𝜑 ∧ ( 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ ) → 𝑆 ⊆ ℂ )
24 2 adantr ( ( 𝜑 ∧ ( 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ ) → 𝑁 ∈ ℕ0 )
25 3 adantr ( ( 𝜑 ∧ ( 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ ) → 𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) )
26 4 adantr ( ( 𝜑 ∧ ( 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ ) → ( 𝐴 “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
27 5 adantr ( ( 𝜑 ∧ ( 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ ) → 0𝑝 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ) )
28 eqid sup ( ( 𝐴 “ ( 𝑆 ∖ { 0 } ) ) , ℝ , < ) = sup ( ( 𝐴 “ ( 𝑆 ∖ { 0 } ) ) , ℝ , < )
29 simpr ( ( 𝜑 ∧ ( 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ ) → ( 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ )
30 23 24 25 26 27 28 29 plyeq0lem ¬ ( 𝜑 ∧ ( 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ )
31 30 pm2.21i ( ( 𝜑 ∧ ( 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ ) → ( 𝐴 “ ( 𝑆 ∖ { 0 } ) ) = ∅ )
32 22 31 pm2.61dane ( 𝜑 → ( 𝐴 “ ( 𝑆 ∖ { 0 } ) ) = ∅ )
33 32 uneq1d ( 𝜑 → ( ( 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ∪ ( 𝐴 “ { 0 } ) ) = ( ∅ ∪ ( 𝐴 “ { 0 } ) ) )
34 undif1 ( ( 𝑆 ∖ { 0 } ) ∪ { 0 } ) = ( 𝑆 ∪ { 0 } )
35 34 imaeq2i ( 𝐴 “ ( ( 𝑆 ∖ { 0 } ) ∪ { 0 } ) ) = ( 𝐴 “ ( 𝑆 ∪ { 0 } ) )
36 imaundi ( 𝐴 “ ( ( 𝑆 ∖ { 0 } ) ∪ { 0 } ) ) = ( ( 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ∪ ( 𝐴 “ { 0 } ) )
37 35 36 eqtr3i ( 𝐴 “ ( 𝑆 ∪ { 0 } ) ) = ( ( 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ∪ ( 𝐴 “ { 0 } ) )
38 un0 ( ( 𝐴 “ { 0 } ) ∪ ∅ ) = ( 𝐴 “ { 0 } )
39 uncom ( ( 𝐴 “ { 0 } ) ∪ ∅ ) = ( ∅ ∪ ( 𝐴 “ { 0 } ) )
40 38 39 eqtr3i ( 𝐴 “ { 0 } ) = ( ∅ ∪ ( 𝐴 “ { 0 } ) )
41 33 37 40 3eqtr4g ( 𝜑 → ( 𝐴 “ ( 𝑆 ∪ { 0 } ) ) = ( 𝐴 “ { 0 } ) )
42 21 41 eqtrd ( 𝜑 → dom 𝐴 = ( 𝐴 “ { 0 } ) )
43 eqimss ( dom 𝐴 = ( 𝐴 “ { 0 } ) → dom 𝐴 ⊆ ( 𝐴 “ { 0 } ) )
44 42 43 syl ( 𝜑 → dom 𝐴 ⊆ ( 𝐴 “ { 0 } ) )
45 15 ffund ( 𝜑 → Fun 𝐴 )
46 ssid dom 𝐴 ⊆ dom 𝐴
47 funimass3 ( ( Fun 𝐴 ∧ dom 𝐴 ⊆ dom 𝐴 ) → ( ( 𝐴 “ dom 𝐴 ) ⊆ { 0 } ↔ dom 𝐴 ⊆ ( 𝐴 “ { 0 } ) ) )
48 45 46 47 sylancl ( 𝜑 → ( ( 𝐴 “ dom 𝐴 ) ⊆ { 0 } ↔ dom 𝐴 ⊆ ( 𝐴 “ { 0 } ) ) )
49 44 48 mpbird ( 𝜑 → ( 𝐴 “ dom 𝐴 ) ⊆ { 0 } )
50 17 49 eqsstrrid ( 𝜑 → ran 𝐴 ⊆ { 0 } )
51 df-f ( 𝐴 : ℕ0 ⟶ { 0 } ↔ ( 𝐴 Fn ℕ0 ∧ ran 𝐴 ⊆ { 0 } ) )
52 16 50 51 sylanbrc ( 𝜑𝐴 : ℕ0 ⟶ { 0 } )
53 c0ex 0 ∈ V
54 53 fconst2 ( 𝐴 : ℕ0 ⟶ { 0 } ↔ 𝐴 = ( ℕ0 × { 0 } ) )
55 52 54 sylib ( 𝜑𝐴 = ( ℕ0 × { 0 } ) )