Metamath Proof Explorer

Theorem linply

Description: A linear polynomial over a subset of the complex numbers is a polynomial over the subset of the complex numbers. (Contributed by AV, 31-Oct-2026)

Ref Expression
Hypothesis linplyfv.p ⊢ 𝑃 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝐶 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
Assertion linply ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ) → 𝑃 ∈ ( Poly ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 linplyfv.p ⊢ 𝑃 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝐶 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
2 simpl ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ) → 𝑆 ⊆ ℂ )
3 oveq2 ⊢ ( 𝑛 = 1 → ( 0 ... 𝑛 ) = ( 0 ... 1 ) )
4 3 sumeq1d ⊢ ( 𝑛 = 1 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑐 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝑐 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
5 4 mpteq2dv ⊢ ( 𝑛 = 1 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑐 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝑐 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
6 5 eqeq2d ⊢ ( 𝑛 = 1 → ( 𝑃 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑐 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↔ 𝑃 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝑐 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
7 fveq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 ‘ 𝑘 ) = ( 𝐶 ‘ 𝑘 ) )
8 7 oveq1d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑐 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝐶 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
9 8 a1d ⊢ ( 𝑐 = 𝐶 → ( 𝑘 ∈ ( 0 ... 1 ) → ( ( 𝑐 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝐶 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
10 9 ralrimiv ⊢ ( 𝑐 = 𝐶 → ∀ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝑐 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝐶 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
11 10 sumeq2d ⊢ ( 𝑐 = 𝐶 → Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝑐 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝐶 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
12 11 mpteq2dv ⊢ ( 𝑐 = 𝐶 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝑐 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝐶 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
13 12 eqeq2d ⊢ ( 𝑐 = 𝐶 → ( 𝑃 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝑐 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↔ 𝑃 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝐶 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
14 1nn0 ⊢ 1 ∈ ℕ0
15 14 a1i ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ) → 1 ∈ ℕ0 )
16 cnex ⊢ ℂ ∈ V
17 16 ssex ⊢ ( 𝑆 ⊆ ℂ → 𝑆 ∈ V )
18 snex ⊢ { 0 } ∈ V
19 18 a1i ⊢ ( 𝑆 ⊆ ℂ → { 0 } ∈ V )
20 17 19 unexd ⊢ ( 𝑆 ⊆ ℂ → ( 𝑆 ∪ { 0 } ) ∈ V )
21 ssun1 ⊢ 𝑆 ⊆ ( 𝑆 ∪ { 0 } )
22 mapss ⊢ ( ( ( 𝑆 ∪ { 0 } ) ∈ V ∧ 𝑆 ⊆ ( 𝑆 ∪ { 0 } ) ) → ( 𝑆 ↑m ℕ0 ) ⊆ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
23 20 21 22 sylancl ⊢ ( 𝑆 ⊆ ℂ → ( 𝑆 ↑m ℕ0 ) ⊆ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
24 23 sselda ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ) → 𝐶 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
25 1 a1i ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ) → 𝑃 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝐶 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
26 6 13 15 24 25 2rspcedvdw ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ) → ∃ 𝑛 ∈ ℕ0 ∃ 𝑐 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑃 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑐 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
27 elply ⊢ ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ↔ ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑐 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑃 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑐 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
28 2 26 27 sylanbrc ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ) → 𝑃 ∈ ( Poly ‘ 𝑆 ) )