ply1term

Description: A one-term polynomial. (Contributed by Mario Carneiro, 17-Jul-2014)

		Ref	Expression
	Hypothesis	ply1term.1	$⊢ F = (z \in ℂ ⟼ A z^{N})$
	Assertion	ply1term	$⊢ (S \subseteq ℂ \land A \in S \land N \in ℕ_{0}) \to F \in Poly (S)$

Proof

Step	Hyp	Ref	Expression
1		ply1term.1	$⊢ F = (z \in ℂ ⟼ A z^{N})$
2		ssel2	$⊢ (S \subseteq ℂ \land A \in S) \to A \in ℂ$
3	1	ply1termlem	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to F = (z \in ℂ ⟼ \sum_{k = 0}^{N} if (k = N, A, 0) z^{k})$
4	2 3	stoic3	$⊢ (S \subseteq ℂ \land A \in S \land N \in ℕ_{0}) \to F = (z \in ℂ ⟼ \sum_{k = 0}^{N} if (k = N, A, 0) z^{k})$
5		simp1	$⊢ (S \subseteq ℂ \land A \in S \land N \in ℕ_{0}) \to S \subseteq ℂ$
6		0cnd	$⊢ (S \subseteq ℂ \land A \in S \land N \in ℕ_{0}) \to 0 \in ℂ$
7	6	snssd	$⊢ (S \subseteq ℂ \land A \in S \land N \in ℕ_{0}) \to \{0\} \subseteq ℂ$
8	5 7	unssd	$⊢ (S \subseteq ℂ \land A \in S \land N \in ℕ_{0}) \to S \cup \{0\} \subseteq ℂ$
9		simp3	$⊢ (S \subseteq ℂ \land A \in S \land N \in ℕ_{0}) \to N \in ℕ_{0}$
10		simpl2	$⊢ ((S \subseteq ℂ \land A \in S \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to A \in S$
11		elun1	$⊢ A \in S \to A \in (S \cup \{0\})$
12	10 11	syl	$⊢ ((S \subseteq ℂ \land A \in S \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to A \in (S \cup \{0\})$
13		ssun2	$⊢ \{0\} \subseteq S \cup \{0\}$
14		c0ex	$⊢ 0 \in V$
15	14	snss	$⊢ 0 \in (S \cup \{0\}) \leftrightarrow \{0\} \subseteq S \cup \{0\}$
16	13 15	mpbir	$⊢ 0 \in (S \cup \{0\})$
17		ifcl	$⊢ (A \in (S \cup \{0\}) \land 0 \in (S \cup \{0\})) \to if (k = N, A, 0) \in (S \cup \{0\})$
18	12 16 17	sylancl	$⊢ ((S \subseteq ℂ \land A \in S \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to if (k = N, A, 0) \in (S \cup \{0\})$
19	8 9 18	elplyd	$⊢ (S \subseteq ℂ \land A \in S \land N \in ℕ_{0}) \to (z \in ℂ ⟼ \sum_{k = 0}^{N} if (k = N, A, 0) z^{k}) \in Poly (S \cup \{0\})$
20	4 19	eqeltrd	$⊢ (S \subseteq ℂ \land A \in S \land N \in ℕ_{0}) \to F \in Poly (S \cup \{0\})$
21		plyun0	$⊢ Poly (S \cup \{0\}) = Poly (S)$
22	20 21	eleqtrdi	$⊢ (S \subseteq ℂ \land A \in S \land N \in ℕ_{0}) \to F \in Poly (S)$

Metamath Proof Explorer

Theorem ply1term

Proof