ply0

Description: The zero function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014)

		Ref	Expression
	Assertion	ply0	$⊢ S \subseteq ℂ \to 0_{𝑝} \in Poly (S)$

Step	Hyp	Ref	Expression
1		df-0p	$⊢ 0_{𝑝} = ℂ \times \{0\}$
2		id	$⊢ S \subseteq ℂ \to S \subseteq ℂ$
3		0cnd	$⊢ S \subseteq ℂ \to 0 \in ℂ$
4	3	snssd	$⊢ S \subseteq ℂ \to \{0\} \subseteq ℂ$
5	2 4	unssd	$⊢ S \subseteq ℂ \to S \cup \{0\} \subseteq ℂ$
6		ssun2	$⊢ \{0\} \subseteq S \cup \{0\}$
7		c0ex	$⊢ 0 \in V$
8	7	snss	$⊢ 0 \in (S \cup \{0\}) \leftrightarrow \{0\} \subseteq S \cup \{0\}$
9	6 8	mpbir	$⊢ 0 \in (S \cup \{0\})$
10		plyconst	$⊢ (S \cup \{0\} \subseteq ℂ \land 0 \in (S \cup \{0\})) \to ℂ \times \{0\} \in Poly (S \cup \{0\})$
11	5 9 10	sylancl	$⊢ S \subseteq ℂ \to ℂ \times \{0\} \in Poly (S \cup \{0\})$
12	1 11	eqeltrid	$⊢ S \subseteq ℂ \to 0_{𝑝} \in Poly (S \cup \{0\})$
13		plyun0	$⊢ Poly (S \cup \{0\}) = Poly (S)$
14	12 13	eleqtrdi	$⊢ S \subseteq ℂ \to 0_{𝑝} \in Poly (S)$

Metamath Proof Explorer