plyid

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

		Ref	Expression
	Assertion	plyid	$⊢ (S \subseteq ℂ \land 1 \in S) \to X^{p} \in Poly (S)$

Step	Hyp	Ref	Expression
1		mptresid	$⊢ {I ↾}_{ℂ} = (z \in ℂ ⟼ z)$
2		df-idp	$⊢ X^{p} = {I ↾}_{ℂ}$
3		exp1	$⊢ z \in ℂ \to z^{1} = z$
4	3	mpteq2ia	$⊢ (z \in ℂ ⟼ z^{1}) = (z \in ℂ ⟼ z)$
5	1 2 4	3eqtr4i	$⊢ X^{p} = (z \in ℂ ⟼ z^{1})$
6		1nn0	$⊢ 1 \in ℕ_{0}$
7		plypow	$⊢ (S \subseteq ℂ \land 1 \in S \land 1 \in ℕ_{0}) \to (z \in ℂ ⟼ z^{1}) \in Poly (S)$
8	6 7	mp3an3	$⊢ (S \subseteq ℂ \land 1 \in S) \to (z \in ℂ ⟼ z^{1}) \in Poly (S)$
9	5 8	eqeltrid	$⊢ (S \subseteq ℂ \land 1 \in S) \to X^{p} \in Poly (S)$

Metamath Proof Explorer