elplyd

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

	Ref	Expression
Hypotheses	elplyd.1	$⊢ φ \to S \subseteq ℂ$
	elplyd.2	$⊢ φ \to N \in ℕ_{0}$
	elplyd.3	$⊢ (φ \land k \in (0 \dots N)) \to A \in S$
Assertion	elplyd	$⊢ φ \to (z \in ℂ ⟼ \sum_{k = 0}^{N} A z^{k}) \in Poly (S)$

Proof

Step	Hyp	Ref	Expression
1		elplyd.1	$⊢ φ \to S \subseteq ℂ$
2		elplyd.2	$⊢ φ \to N \in ℕ_{0}$
3		elplyd.3	$⊢ (φ \land k \in (0 \dots N)) \to A \in S$
4		fveq2	$⊢ j = k \to (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0)) (j) = (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0)) (k)$
5		oveq2	$⊢ j = k \to z^{j} = z^{k}$
6	4 5	oveq12d	$⊢ j = k \to (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0)) (j) z^{j} = (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0)) (k) z^{k}$
7		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0)) (j)$
8		nfcv	$⊢ \underline{Ⅎ} k \times$
9		nfcv	$⊢ \underline{Ⅎ} k z^{j}$
10	7 8 9	nfov	$⊢ \underline{Ⅎ} k (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0)) (j) z^{j}$
11		nfcv	$⊢ \underline{Ⅎ} j (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0)) (k) z^{k}$
12	6 10 11	cbvsum	$⊢ \sum_{j = 0}^{N} (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0)) (j) z^{j} = \sum_{k = 0}^{N} (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0)) (k) z^{k}$
13		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
14		iftrue	$⊢ k \in (0 \dots N) \to if (k \in (0 \dots N), A, 0) = A$
15	14	adantl	$⊢ (φ \land k \in (0 \dots N)) \to if (k \in (0 \dots N), A, 0) = A$
16	15 3	eqeltrd	$⊢ (φ \land k \in (0 \dots N)) \to if (k \in (0 \dots N), A, 0) \in S$
17		eqid	$⊢ (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0)) = (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0))$
18	17	fvmpt2	$⊢ (k \in ℕ_{0} \land if (k \in (0 \dots N), A, 0) \in S) \to (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0)) (k) = if (k \in (0 \dots N), A, 0)$
19	13 16 18	syl2an2	$⊢ (φ \land k \in (0 \dots N)) \to (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0)) (k) = if (k \in (0 \dots N), A, 0)$
20	19 15	eqtrd	$⊢ (φ \land k \in (0 \dots N)) \to (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0)) (k) = A$
21	20	oveq1d	$⊢ (φ \land k \in (0 \dots N)) \to (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0)) (k) z^{k} = A z^{k}$
22	21	sumeq2dv	$⊢ φ \to \sum_{k = 0}^{N} (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0)) (k) z^{k} = \sum_{k = 0}^{N} A z^{k}$
23	12 22	eqtrid	$⊢ φ \to \sum_{j = 0}^{N} (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0)) (j) z^{j} = \sum_{k = 0}^{N} A z^{k}$
24	23	mpteq2dv	$⊢ φ \to (z \in ℂ ⟼ \sum_{j = 0}^{N} (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0)) (j) z^{j}) = (z \in ℂ ⟼ \sum_{k = 0}^{N} A z^{k})$
25		0cnd	$⊢ φ \to 0 \in ℂ$
26	25	snssd	$⊢ φ \to \{0\} \subseteq ℂ$
27	1 26	unssd	$⊢ φ \to S \cup \{0\} \subseteq ℂ$
28		elun1	$⊢ A \in S \to A \in (S \cup \{0\})$
29	3 28	syl	$⊢ (φ \land k \in (0 \dots N)) \to A \in (S \cup \{0\})$
30	29	adantlr	$⊢ ((φ \land k \in ℕ_{0}) \land k \in (0 \dots N)) \to A \in (S \cup \{0\})$
31		ssun2	$⊢ \{0\} \subseteq S \cup \{0\}$
32		c0ex	$⊢ 0 \in V$
33	32	snss	$⊢ 0 \in (S \cup \{0\}) \leftrightarrow \{0\} \subseteq S \cup \{0\}$
34	31 33	mpbir	$⊢ 0 \in (S \cup \{0\})$
35	34	a1i	$⊢ ((φ \land k \in ℕ_{0}) \land \neg k \in (0 \dots N)) \to 0 \in (S \cup \{0\})$
36	30 35	ifclda	$⊢ (φ \land k \in ℕ_{0}) \to if (k \in (0 \dots N), A, 0) \in (S \cup \{0\})$
37	36	fmpttd	$⊢ φ \to (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0)) : ℕ_{0} ⟶ S \cup \{0\}$
38		elplyr	$⊢ (S \cup \{0\} \subseteq ℂ \land N \in ℕ_{0} \land (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0)) : ℕ_{0} ⟶ S \cup \{0\}) \to (z \in ℂ ⟼ \sum_{j = 0}^{N} (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0)) (j) z^{j}) \in Poly (S \cup \{0\})$
39	27 2 37 38	syl3anc	$⊢ φ \to (z \in ℂ ⟼ \sum_{j = 0}^{N} (k \in ℕ_{0} ⟼ if (k \in (0 \dots N), A, 0)) (j) z^{j}) \in Poly (S \cup \{0\})$
40	24 39	eqeltrrd	$⊢ φ \to (z \in ℂ ⟼ \sum_{k = 0}^{N} A z^{k}) \in Poly (S \cup \{0\})$
41		plyun0	$⊢ Poly (S \cup \{0\}) = Poly (S)$
42	40 41	eleqtrdi	$⊢ φ \to (z \in ℂ ⟼ \sum_{k = 0}^{N} A z^{k}) \in Poly (S)$

Metamath Proof Explorer

Theorem elplyd

Proof