Metamath Proof Explorer

Theorem linplyfv

Description: The evaluation of a linear polynomial over a subset of the complex numbers at a complex number. (Contributed by AV, 31-Oct-2026)

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

Proof

Step Hyp Ref Expression
1 linplyfv.p ⊢ 𝑃 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝐶 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
2 1 a1i ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → 𝑃 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝐶 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
3 oveq1 ⊢ ( 𝑧 = 𝑋 → ( 𝑧 ↑ 𝑘 ) = ( 𝑋 ↑ 𝑘 ) )
4 3 oveq2d ⊢ ( 𝑧 = 𝑋 → ( ( 𝐶 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝐶 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) )
5 4 a1d ⊢ ( 𝑧 = 𝑋 → ( 𝑘 ∈ ( 0 ... 1 ) → ( ( 𝐶 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝐶 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) )
6 5 ralrimiv ⊢ ( 𝑧 = 𝑋 → ∀ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝐶 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝐶 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) )
7 6 sumeq2d ⊢ ( 𝑧 = 𝑋 → Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝐶 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝐶 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) )
8 fz01pr ⊢ ( 0 ... 1 ) = { 0 , 1 }
9 8 sumeq1i ⊢ Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝐶 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) = Σ 𝑘 ∈ { 0 , 1 } ( ( 𝐶 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) )
10 fveq2 ⊢ ( 𝑘 = 0 → ( 𝐶 ‘ 𝑘 ) = ( 𝐶 ‘ 0 ) )
11 oveq2 ⊢ ( 𝑘 = 0 → ( 𝑋 ↑ 𝑘 ) = ( 𝑋 ↑ 0 ) )
12 10 11 oveq12d ⊢ ( 𝑘 = 0 → ( ( 𝐶 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) = ( ( 𝐶 ‘ 0 ) · ( 𝑋 ↑ 0 ) ) )
13 fveq2 ⊢ ( 𝑘 = 1 → ( 𝐶 ‘ 𝑘 ) = ( 𝐶 ‘ 1 ) )
14 oveq2 ⊢ ( 𝑘 = 1 → ( 𝑋 ↑ 𝑘 ) = ( 𝑋 ↑ 1 ) )
15 13 14 oveq12d ⊢ ( 𝑘 = 1 → ( ( 𝐶 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) = ( ( 𝐶 ‘ 1 ) · ( 𝑋 ↑ 1 ) ) )
16 cnex ⊢ ℂ ∈ V
17 simp1 ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → 𝑆 ⊆ ℂ )
18 mapss ⊢ ( ( ℂ ∈ V ∧ 𝑆 ⊆ ℂ ) → ( 𝑆 ↑m ℕ0 ) ⊆ ( ℂ ↑m ℕ0 ) )
19 16 17 18 sylancr ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → ( 𝑆 ↑m ℕ0 ) ⊆ ( ℂ ↑m ℕ0 ) )
20 simp2 ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) )
21 19 20 sseldd ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → 𝐶 ∈ ( ℂ ↑m ℕ0 ) )
22 21 elmaprd ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → 𝐶 : ℕ0 ⟶ ℂ )
23 0nn0 ⊢ 0 ∈ ℕ0
24 23 a1i ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → 0 ∈ ℕ0 )
25 22 24 ffvelcdmd ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → ( 𝐶 ‘ 0 ) ∈ ℂ )
26 id ⊢ ( 𝑋 ∈ ℂ → 𝑋 ∈ ℂ )
27 23 a1i ⊢ ( 𝑋 ∈ ℂ → 0 ∈ ℕ0 )
28 26 27 expcld ⊢ ( 𝑋 ∈ ℂ → ( 𝑋 ↑ 0 ) ∈ ℂ )
29 28 3ad2ant3 ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → ( 𝑋 ↑ 0 ) ∈ ℂ )
30 25 29 mulcld ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → ( ( 𝐶 ‘ 0 ) · ( 𝑋 ↑ 0 ) ) ∈ ℂ )
31 1nn0 ⊢ 1 ∈ ℕ0
32 31 a1i ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → 1 ∈ ℕ0 )
33 22 32 ffvelcdmd ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → ( 𝐶 ‘ 1 ) ∈ ℂ )
34 31 a1i ⊢ ( 𝑋 ∈ ℂ → 1 ∈ ℕ0 )
35 26 34 expcld ⊢ ( 𝑋 ∈ ℂ → ( 𝑋 ↑ 1 ) ∈ ℂ )
36 35 3ad2ant3 ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → ( 𝑋 ↑ 1 ) ∈ ℂ )
37 33 36 mulcld ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → ( ( 𝐶 ‘ 1 ) · ( 𝑋 ↑ 1 ) ) ∈ ℂ )
38 30 37 jca ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → ( ( ( 𝐶 ‘ 0 ) · ( 𝑋 ↑ 0 ) ) ∈ ℂ ∧ ( ( 𝐶 ‘ 1 ) · ( 𝑋 ↑ 1 ) ) ∈ ℂ ) )
39 0z ⊢ 0 ∈ ℤ
40 1z ⊢ 1 ∈ ℤ
41 39 40 pm3.2i ⊢ ( 0 ∈ ℤ ∧ 1 ∈ ℤ )
42 41 a1i ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → ( 0 ∈ ℤ ∧ 1 ∈ ℤ ) )
43 0ne1 ⊢ 0 ≠ 1
44 43 a1i ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → 0 ≠ 1 )
45 12 15 38 42 44 sumpr ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → Σ 𝑘 ∈ { 0 , 1 } ( ( 𝐶 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) = ( ( ( 𝐶 ‘ 0 ) · ( 𝑋 ↑ 0 ) ) + ( ( 𝐶 ‘ 1 ) · ( 𝑋 ↑ 1 ) ) ) )
46 exp0 ⊢ ( 𝑋 ∈ ℂ → ( 𝑋 ↑ 0 ) = 1 )
47 46 3ad2ant3 ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → ( 𝑋 ↑ 0 ) = 1 )
48 47 oveq2d ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → ( ( 𝐶 ‘ 0 ) · ( 𝑋 ↑ 0 ) ) = ( ( 𝐶 ‘ 0 ) · 1 ) )
49 25 mulridd ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → ( ( 𝐶 ‘ 0 ) · 1 ) = ( 𝐶 ‘ 0 ) )
50 48 49 eqtrd ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → ( ( 𝐶 ‘ 0 ) · ( 𝑋 ↑ 0 ) ) = ( 𝐶 ‘ 0 ) )
51 exp1 ⊢ ( 𝑋 ∈ ℂ → ( 𝑋 ↑ 1 ) = 𝑋 )
52 51 3ad2ant3 ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → ( 𝑋 ↑ 1 ) = 𝑋 )
53 52 oveq2d ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → ( ( 𝐶 ‘ 1 ) · ( 𝑋 ↑ 1 ) ) = ( ( 𝐶 ‘ 1 ) · 𝑋 ) )
54 50 53 oveq12d ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → ( ( ( 𝐶 ‘ 0 ) · ( 𝑋 ↑ 0 ) ) + ( ( 𝐶 ‘ 1 ) · ( 𝑋 ↑ 1 ) ) ) = ( ( 𝐶 ‘ 0 ) + ( ( 𝐶 ‘ 1 ) · 𝑋 ) ) )
55 45 54 eqtrd ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → Σ 𝑘 ∈ { 0 , 1 } ( ( 𝐶 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) = ( ( 𝐶 ‘ 0 ) + ( ( 𝐶 ‘ 1 ) · 𝑋 ) ) )
56 9 55 eqtrid ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝐶 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) = ( ( 𝐶 ‘ 0 ) + ( ( 𝐶 ‘ 1 ) · 𝑋 ) ) )
57 7 56 sylan9eqr ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) ∧ 𝑧 = 𝑋 ) → Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝐶 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝐶 ‘ 0 ) + ( ( 𝐶 ‘ 1 ) · 𝑋 ) ) )
58 simp3 ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → 𝑋 ∈ ℂ )
59 ovexd ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → ( ( 𝐶 ‘ 0 ) + ( ( 𝐶 ‘ 1 ) · 𝑋 ) ) ∈ V )
60 2 57 58 59 fvmptd ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → ( 𝑃 ‘ 𝑋 ) = ( ( 𝐶 ‘ 0 ) + ( ( 𝐶 ‘ 1 ) · 𝑋 ) ) )