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 ⊢ P = z ∈ ℂ ⟼ ∑ k = 0 1 C ⁡ k ⁢ z k
Assertion linplyfv ⊢ S ⊆ ℂ ∧ C ∈ S ℕ 0 ∧ X ∈ ℂ → P ⁡ X = C ⁡ 0 + C ⁡ 1 ⁢ X

Proof

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