# 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$