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

Proof

Step Hyp Ref Expression
1 linplyfv.p ⊢ P = z ∈ ℂ ⟼ ∑ k = 0 1 C ⁡ k ⁢ z k
2 simpl ⊢ S ⊆ ℂ ∧ C ∈ S ℕ 0 → S ⊆ ℂ
3 oveq2 ⊢ n = 1 → 0 … n = 0 … 1
4 3 sumeq1d ⊢ n = 1 → ∑ k = 0 n c ⁡ k ⁢ z k = ∑ k = 0 1 c ⁡ k ⁢ z k
5 4 mpteq2dv ⊢ n = 1 → z ∈ ℂ ⟼ ∑ k = 0 n c ⁡ k ⁢ z k = z ∈ ℂ ⟼ ∑ k = 0 1 c ⁡ k ⁢ z k
6 5 eqeq2d ⊢ n = 1 → P = z ∈ ℂ ⟼ ∑ k = 0 n c ⁡ k ⁢ z k ↔ P = z ∈ ℂ ⟼ ∑ k = 0 1 c ⁡ k ⁢ z k
7 fveq1 ⊢ c = C → c ⁡ k = C ⁡ k
8 7 oveq1d ⊢ c = C → c ⁡ k ⁢ z k = C ⁡ k ⁢ z k
9 8 a1d ⊢ c = C → k ∈ 0 … 1 → c ⁡ k ⁢ z k = C ⁡ k ⁢ z k
10 9 ralrimiv ⊢ c = C → ∀ k ∈ 0 … 1 c ⁡ k ⁢ z k = C ⁡ k ⁢ z k
11 10 sumeq2d ⊢ c = C → ∑ k = 0 1 c ⁡ k ⁢ z k = ∑ k = 0 1 C ⁡ k ⁢ z k
12 11 mpteq2dv ⊢ c = C → z ∈ ℂ ⟼ ∑ k = 0 1 c ⁡ k ⁢ z k = z ∈ ℂ ⟼ ∑ k = 0 1 C ⁡ k ⁢ z k
13 12 eqeq2d ⊢ c = C → P = z ∈ ℂ ⟼ ∑ k = 0 1 c ⁡ k ⁢ z k ↔ P = z ∈ ℂ ⟼ ∑ k = 0 1 C ⁡ k ⁢ z k
14 1nn0 ⊢ 1 ∈ ℕ 0
15 14 a1i ⊢ S ⊆ ℂ ∧ C ∈ S ℕ 0 → 1 ∈ ℕ 0
16 cnex ⊢ ℂ ∈ V
17 16 ssex ⊢ S ⊆ ℂ → S ∈ V
18 snex ⊢ 0 ∈ V
19 18 a1i ⊢ S ⊆ ℂ → 0 ∈ V
20 17 19 unexd ⊢ S ⊆ ℂ → S ∪ 0 ∈ V
21 ssun1 ⊢ S ⊆ S ∪ 0
22 mapss ⊢ S ∪ 0 ∈ V ∧ S ⊆ S ∪ 0 → S ℕ 0 ⊆ S ∪ 0 ℕ 0
23 20 21 22 sylancl ⊢ S ⊆ ℂ → S ℕ 0 ⊆ S ∪ 0 ℕ 0
24 23 sselda ⊢ S ⊆ ℂ ∧ C ∈ S ℕ 0 → C ∈ S ∪ 0 ℕ 0
25 1 a1i ⊢ S ⊆ ℂ ∧ C ∈ S ℕ 0 → P = z ∈ ℂ ⟼ ∑ k = 0 1 C ⁡ k ⁢ z k
26 6 13 15 24 25 2rspcedvdw ⊢ S ⊆ ℂ ∧ C ∈ S ℕ 0 → ∃ n ∈ ℕ 0 ∃ c ∈ S ∪ 0 ℕ 0 P = z ∈ ℂ ⟼ ∑ k = 0 n c ⁡ k ⁢ z k
27 elply ⊢ P ∈ Poly ⁡ S ↔ S ⊆ ℂ ∧ ∃ n ∈ ℕ 0 ∃ c ∈ S ∪ 0 ℕ 0 P = z ∈ ℂ ⟼ ∑ k = 0 n c ⁡ k ⁢ z k
28 2 26 27 sylanbrc ⊢ S ⊆ ℂ ∧ C ∈ S ℕ 0 → P ∈ Poly ⁡ S