elplyr

Description: Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

		Ref	Expression
	Assertion	elplyr	$⊢ (S \subseteq ℂ \land N \in ℕ_{0} \land A : ℕ_{0} ⟶ S) \to (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k}) \in Poly (S)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (S \subseteq ℂ \land N \in ℕ_{0} \land A : ℕ_{0} ⟶ S) \to S \subseteq ℂ$
2		simp2	$⊢ (S \subseteq ℂ \land N \in ℕ_{0} \land A : ℕ_{0} ⟶ S) \to N \in ℕ_{0}$
3		simp3	$⊢ (S \subseteq ℂ \land N \in ℕ_{0} \land A : ℕ_{0} ⟶ S) \to A : ℕ_{0} ⟶ S$
4		ssun1	$⊢ S \subseteq S \cup \{0\}$
5		fss	$⊢ (A : ℕ_{0} ⟶ S \land S \subseteq S \cup \{0\}) \to A : ℕ_{0} ⟶ S \cup \{0\}$
6	3 4 5	sylancl	$⊢ (S \subseteq ℂ \land N \in ℕ_{0} \land A : ℕ_{0} ⟶ S) \to A : ℕ_{0} ⟶ S \cup \{0\}$
7		0cnd	$⊢ (S \subseteq ℂ \land N \in ℕ_{0} \land A : ℕ_{0} ⟶ S) \to 0 \in ℂ$
8	7	snssd	$⊢ (S \subseteq ℂ \land N \in ℕ_{0} \land A : ℕ_{0} ⟶ S) \to \{0\} \subseteq ℂ$
9	1 8	unssd	$⊢ (S \subseteq ℂ \land N \in ℕ_{0} \land A : ℕ_{0} ⟶ S) \to S \cup \{0\} \subseteq ℂ$
10		cnex	$⊢ ℂ \in V$
11		ssexg	$⊢ (S \cup \{0\} \subseteq ℂ \land ℂ \in V) \to S \cup \{0\} \in V$
12	9 10 11	sylancl	$⊢ (S \subseteq ℂ \land N \in ℕ_{0} \land A : ℕ_{0} ⟶ S) \to S \cup \{0\} \in V$
13		nn0ex	$⊢ ℕ_{0} \in V$
14		elmapg	$⊢ (S \cup \{0\} \in V \land ℕ_{0} \in V) \to (A \in ({(S \cup \{0\})}^{ℕ_{0}}) \leftrightarrow A : ℕ_{0} ⟶ S \cup \{0\})$
15	12 13 14	sylancl	$⊢ (S \subseteq ℂ \land N \in ℕ_{0} \land A : ℕ_{0} ⟶ S) \to (A \in ({(S \cup \{0\})}^{ℕ_{0}}) \leftrightarrow A : ℕ_{0} ⟶ S \cup \{0\})$
16	6 15	mpbird	$⊢ (S \subseteq ℂ \land N \in ℕ_{0} \land A : ℕ_{0} ⟶ S) \to A \in ({(S \cup \{0\})}^{ℕ_{0}})$
17		eqidd	$⊢ (S \subseteq ℂ \land N \in ℕ_{0} \land A : ℕ_{0} ⟶ S) \to (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k})$
18		oveq2	$⊢ n = N \to (0 \dots n) = (0 \dots N)$
19	18	sumeq1d	$⊢ n = N \to \sum_{k = 0}^{n} a (k) z^{k} = \sum_{k = 0}^{N} a (k) z^{k}$
20	19	mpteq2dv	$⊢ n = N \to (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{N} a (k) z^{k})$
21	20	eqeq2d	$⊢ n = N \to ((z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}) \leftrightarrow (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{N} a (k) z^{k}))$
22		fveq1	$⊢ a = A \to a (k) = A (k)$
23	22	oveq1d	$⊢ a = A \to a (k) z^{k} = A (k) z^{k}$
24	23	sumeq2sdv	$⊢ a = A \to \sum_{k = 0}^{N} a (k) z^{k} = \sum_{k = 0}^{N} A (k) z^{k}$
25	24	mpteq2dv	$⊢ a = A \to (z \in ℂ ⟼ \sum_{k = 0}^{N} a (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k})$
26	25	eqeq2d	$⊢ a = A \to ((z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{N} a (k) z^{k}) \leftrightarrow (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k}))$
27	21 26	rspc2ev	$⊢ (N \in ℕ_{0} \land A \in ({(S \cup \{0\})}^{ℕ_{0}}) \land (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k})) \to \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})$
28	2 16 17 27	syl3anc	$⊢ (S \subseteq ℂ \land N \in ℕ_{0} \land A : ℕ_{0} ⟶ S) \to \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})$
29		elply	$⊢ (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k}) \in Poly (S) \leftrightarrow (S \subseteq ℂ \land \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))$
30	1 28 29	sylanbrc	$⊢ (S \subseteq ℂ \land N \in ℕ_{0} \land A : ℕ_{0} ⟶ S) \to (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k}) \in Poly (S)$

Metamath Proof Explorer

Theorem elplyr

Proof