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 ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃! 𝑎 ∈ ( ℂ ↑m0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 plyssc ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
2 1 sseli ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
3 elply2 ( 𝐹 ∈ ( Poly ‘ ℂ ) ↔ ( ℂ ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0𝑎 ∈ ( ( ℂ ∪ { 0 } ) ↑m0 ) ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) )
4 3 simprbi ( 𝐹 ∈ ( Poly ‘ ℂ ) → ∃ 𝑛 ∈ ℕ0𝑎 ∈ ( ( ℂ ∪ { 0 } ) ↑m0 ) ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
5 rexcom ( ∃ 𝑛 ∈ ℕ0𝑎 ∈ ( ( ℂ ∪ { 0 } ) ↑m0 ) ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ↔ ∃ 𝑎 ∈ ( ( ℂ ∪ { 0 } ) ↑m0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
6 4 5 sylib ( 𝐹 ∈ ( Poly ‘ ℂ ) → ∃ 𝑎 ∈ ( ( ℂ ∪ { 0 } ) ↑m0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
7 2 6 syl ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑎 ∈ ( ( ℂ ∪ { 0 } ) ↑m0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
8 0cn 0 ∈ ℂ
9 snssi ( 0 ∈ ℂ → { 0 } ⊆ ℂ )
10 8 9 ax-mp { 0 } ⊆ ℂ
11 ssequn2 ( { 0 } ⊆ ℂ ↔ ( ℂ ∪ { 0 } ) = ℂ )
12 10 11 mpbi ( ℂ ∪ { 0 } ) = ℂ
13 12 oveq1i ( ( ℂ ∪ { 0 } ) ↑m0 ) = ( ℂ ↑m0 )
14 13 rexeqi ( ∃ 𝑎 ∈ ( ( ℂ ∪ { 0 } ) ↑m0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ↔ ∃ 𝑎 ∈ ( ℂ ↑m0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
15 7 14 sylib ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑎 ∈ ( ℂ ↑m0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
16 reeanv ( ∃ 𝑛 ∈ ℕ0𝑚 ∈ ℕ0 ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ↔ ( ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ∃ 𝑚 ∈ ℕ0 ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) )
17 simp1l ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m0 ) ∧ 𝑏 ∈ ( ℂ ↑m0 ) ) ) ∧ ( 𝑛 ∈ ℕ0𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
18 simp1rl ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m0 ) ∧ 𝑏 ∈ ( ℂ ↑m0 ) ) ) ∧ ( 𝑛 ∈ ℕ0𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → 𝑎 ∈ ( ℂ ↑m0 ) )
19 simp1rr ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m0 ) ∧ 𝑏 ∈ ( ℂ ↑m0 ) ) ) ∧ ( 𝑛 ∈ ℕ0𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → 𝑏 ∈ ( ℂ ↑m0 ) )
20 simp2l ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m0 ) ∧ 𝑏 ∈ ( ℂ ↑m0 ) ) ) ∧ ( 𝑛 ∈ ℕ0𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → 𝑛 ∈ ℕ0 )
21 simp2r ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m0 ) ∧ 𝑏 ∈ ( ℂ ↑m0 ) ) ) ∧ ( 𝑛 ∈ ℕ0𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → 𝑚 ∈ ℕ0 )
22 simp3ll ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m0 ) ∧ 𝑏 ∈ ( ℂ ↑m0 ) ) ) ∧ ( 𝑛 ∈ ℕ0𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } )
23 simp3rl ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m0 ) ∧ 𝑏 ∈ ( ℂ ↑m0 ) ) ) ∧ ( 𝑛 ∈ ℕ0𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } )
24 simp3lr ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m0 ) ∧ 𝑏 ∈ ( ℂ ↑m0 ) ) ) ∧ ( 𝑛 ∈ ℕ0𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) )
25 oveq1 ( 𝑧 = 𝑤 → ( 𝑧𝑘 ) = ( 𝑤𝑘 ) )
26 25 oveq2d ( 𝑧 = 𝑤 → ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) = ( ( 𝑎𝑘 ) · ( 𝑤𝑘 ) ) )
27 26 sumeq2sdv ( 𝑧 = 𝑤 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑤𝑘 ) ) )
28 fveq2 ( 𝑘 = 𝑗 → ( 𝑎𝑘 ) = ( 𝑎𝑗 ) )
29 oveq2 ( 𝑘 = 𝑗 → ( 𝑤𝑘 ) = ( 𝑤𝑗 ) )
30 28 29 oveq12d ( 𝑘 = 𝑗 → ( ( 𝑎𝑘 ) · ( 𝑤𝑘 ) ) = ( ( 𝑎𝑗 ) · ( 𝑤𝑗 ) ) )
31 30 cbvsumv Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑤𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑗 ) · ( 𝑤𝑗 ) )
32 27 31 eqtrdi ( 𝑧 = 𝑤 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑗 ) · ( 𝑤𝑗 ) ) )
33 32 cbvmptv ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) = ( 𝑤 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑗 ) · ( 𝑤𝑗 ) ) )
34 24 33 eqtrdi ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m0 ) ∧ 𝑏 ∈ ( ℂ ↑m0 ) ) ) ∧ ( 𝑛 ∈ ℕ0𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → 𝐹 = ( 𝑤 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑗 ) · ( 𝑤𝑗 ) ) ) )
35 simp3rr ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m0 ) ∧ 𝑏 ∈ ( ℂ ↑m0 ) ) ) ∧ ( 𝑛 ∈ ℕ0𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) )
36 25 oveq2d ( 𝑧 = 𝑤 → ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) = ( ( 𝑏𝑘 ) · ( 𝑤𝑘 ) ) )
37 36 sumeq2sdv ( 𝑧 = 𝑤 → Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑤𝑘 ) ) )
38 fveq2 ( 𝑘 = 𝑗 → ( 𝑏𝑘 ) = ( 𝑏𝑗 ) )
39 38 29 oveq12d ( 𝑘 = 𝑗 → ( ( 𝑏𝑘 ) · ( 𝑤𝑘 ) ) = ( ( 𝑏𝑗 ) · ( 𝑤𝑗 ) ) )
40 39 cbvsumv Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑤𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑗 ) · ( 𝑤𝑗 ) )
41 37 40 eqtrdi ( 𝑧 = 𝑤 → Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑗 ) · ( 𝑤𝑗 ) ) )
42 41 cbvmptv ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) = ( 𝑤 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑗 ) · ( 𝑤𝑗 ) ) )
43 35 42 eqtrdi ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m0 ) ∧ 𝑏 ∈ ( ℂ ↑m0 ) ) ) ∧ ( 𝑛 ∈ ℕ0𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → 𝐹 = ( 𝑤 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑗 ) · ( 𝑤𝑗 ) ) ) )
44 17 18 19 20 21 22 23 34 43 coeeulem ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m0 ) ∧ 𝑏 ∈ ( ℂ ↑m0 ) ) ) ∧ ( 𝑛 ∈ ℕ0𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) ) → 𝑎 = 𝑏 )
45 44 3expia ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m0 ) ∧ 𝑏 ∈ ( ℂ ↑m0 ) ) ) ∧ ( 𝑛 ∈ ℕ0𝑚 ∈ ℕ0 ) ) → ( ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → 𝑎 = 𝑏 ) )
46 45 rexlimdvva ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m0 ) ∧ 𝑏 ∈ ( ℂ ↑m0 ) ) ) → ( ∃ 𝑛 ∈ ℕ0𝑚 ∈ ℕ0 ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → 𝑎 = 𝑏 ) )
47 16 46 syl5bir ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m0 ) ∧ 𝑏 ∈ ( ℂ ↑m0 ) ) ) → ( ( ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ∃ 𝑚 ∈ ℕ0 ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → 𝑎 = 𝑏 ) )
48 47 ralrimivva ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∀ 𝑎 ∈ ( ℂ ↑m0 ) ∀ 𝑏 ∈ ( ℂ ↑m0 ) ( ( ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ∃ 𝑚 ∈ ℕ0 ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → 𝑎 = 𝑏 ) )
49 imaeq1 ( 𝑎 = 𝑏 → ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) )
50 49 eqeq1d ( 𝑎 = 𝑏 → ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ↔ ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ) )
51 fveq1 ( 𝑎 = 𝑏 → ( 𝑎𝑘 ) = ( 𝑏𝑘 ) )
52 51 oveq1d ( 𝑎 = 𝑏 → ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) = ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) )
53 52 sumeq2sdv ( 𝑎 = 𝑏 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) )
54 53 mpteq2dv ( 𝑎 = 𝑏 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) )
55 54 eqeq2d ( 𝑎 = 𝑏 → ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ↔ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
56 50 55 anbi12d ( 𝑎 = 𝑏 → ( ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ↔ ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) )
57 56 rexbidv ( 𝑎 = 𝑏 → ( ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ0 ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) )
58 fvoveq1 ( 𝑛 = 𝑚 → ( ℤ ‘ ( 𝑛 + 1 ) ) = ( ℤ ‘ ( 𝑚 + 1 ) ) )
59 58 imaeq2d ( 𝑛 = 𝑚 → ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) )
60 59 eqeq1d ( 𝑛 = 𝑚 → ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ↔ ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ) )
61 oveq2 ( 𝑛 = 𝑚 → ( 0 ... 𝑛 ) = ( 0 ... 𝑚 ) )
62 61 sumeq1d ( 𝑛 = 𝑚 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) )
63 62 mpteq2dv ( 𝑛 = 𝑚 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) )
64 63 eqeq2d ( 𝑛 = 𝑚 → ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ↔ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
65 60 64 anbi12d ( 𝑛 = 𝑚 → ( ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ↔ ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) )
66 65 cbvrexvw ( ∃ 𝑛 ∈ ℕ0 ( ( 𝑏 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ↔ ∃ 𝑚 ∈ ℕ0 ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
67 57 66 bitrdi ( 𝑎 = 𝑏 → ( ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ↔ ∃ 𝑚 ∈ ℕ0 ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) )
68 67 reu4 ( ∃! 𝑎 ∈ ( ℂ ↑m0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ↔ ( ∃ 𝑎 ∈ ( ℂ ↑m0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ∀ 𝑎 ∈ ( ℂ ↑m0 ) ∀ 𝑏 ∈ ( ℂ ↑m0 ) ( ( ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ∧ ∃ 𝑚 ∈ ℕ0 ( ( 𝑏 “ ( ℤ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏𝑘 ) · ( 𝑧𝑘 ) ) ) ) ) → 𝑎 = 𝑏 ) ) )
69 15 48 68 sylanbrc ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃! 𝑎 ∈ ( ℂ ↑m0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) )