This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elply

Description: Definition of a polynomial with coefficients in S . (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Assertion elply ⊢ F ∈ Poly ⁡ S ↔ S ⊆ ℂ ∧ ∃ n ∈ ℕ 0 ∃ a ∈ S ∪ 0 ℕ 0 F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k

Proof

Step Hyp Ref Expression
1 plybss ⊢ F ∈ Poly ⁡ S → S ⊆ ℂ
2 plyval ⊢ S ⊆ ℂ → Poly ⁡ S = f | ∃ n ∈ ℕ 0 ∃ a ∈ S ∪ 0 ℕ 0 f = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k
3 2 eleq2d ⊢ S ⊆ ℂ → F ∈ Poly ⁡ S ↔ F ∈ f | ∃ n ∈ ℕ 0 ∃ a ∈ S ∪ 0 ℕ 0 f = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k
4 id ⊢ F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k → F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k
5 cnex ⊢ ℂ ∈ V
6 5 mptex ⊢ z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k ∈ V
7 4 6 eqeltrdi ⊢ F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k → F ∈ V
8 7 a1i ⊢ n ∈ ℕ 0 ∧ a ∈ S ∪ 0 ℕ 0 → F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k → F ∈ V
9 8 rexlimivv ⊢ ∃ n ∈ ℕ 0 ∃ a ∈ S ∪ 0 ℕ 0 F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k → F ∈ V
10 eqeq1 ⊢ f = F → f = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k ↔ F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k
11 10 2rexbidv ⊢ f = F → ∃ n ∈ ℕ 0 ∃ a ∈ S ∪ 0 ℕ 0 f = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k ↔ ∃ n ∈ ℕ 0 ∃ a ∈ S ∪ 0 ℕ 0 F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k
12 9 11 elab3 ⊢ F ∈ f | ∃ n ∈ ℕ 0 ∃ a ∈ S ∪ 0 ℕ 0 f = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k ↔ ∃ n ∈ ℕ 0 ∃ a ∈ S ∪ 0 ℕ 0 F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k
13 3 12 bitrdi ⊢ S ⊆ ℂ → F ∈ Poly ⁡ S ↔ ∃ n ∈ ℕ 0 ∃ a ∈ S ∪ 0 ℕ 0 F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k
14 1 13 biadanii ⊢ F ∈ Poly ⁡ S ↔ S ⊆ ℂ ∧ ∃ n ∈ ℕ 0 ∃ a ∈ S ∪ 0 ℕ 0 F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k