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 } ) ↑m ℕ0 ) )
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 } ) ↑m ℕ0 ) )
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 } ) ↑m ℕ0 ) ↔ 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
14 11 12 13 sylancl ⊢ ( 𝜑 → ( 𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ↔ 𝐴 : ℕ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 } ) ↑m ℕ0 ) )
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 } ) )