Theorem plyid

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

	Ref	Expression
Assertion	plyid	⊢ ( ( 𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆 ) → Xp ∈ ( Poly ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		mptresid	⊢ ( I ↾ ℂ ) = ( 𝑧 ∈ ℂ ↦ 𝑧 )
2		df-idp	⊢ Xp = ( I ↾ ℂ )
3		exp1	⊢ ( 𝑧 ∈ ℂ → ( 𝑧 ↑ 1 ) = 𝑧 )
4	3	mpteq2ia	⊢ ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 1 ) ) = ( 𝑧 ∈ ℂ ↦ 𝑧 )
5	1 2 4	3eqtr4i	⊢ Xp = ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 1 ) )
6		1nn0	⊢ 1 ∈ ℕ0
7		plypow	⊢ ( ( 𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆 ∧ 1 ∈ ℕ0 ) → ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 1 ) ) ∈ ( Poly ‘ 𝑆 ) )
8	6 7	mp3an3	⊢ ( ( 𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆 ) → ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 1 ) ) ∈ ( Poly ‘ 𝑆 ) )
9	5 8	eqeltrid	⊢ ( ( 𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆 ) → Xp ∈ ( Poly ‘ 𝑆 ) )