Theorem coeidp

Description: The coefficients of the identity function. (Contributed by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Assertion	coeidp	⊢ ( 𝐴 ∈ ℕ0 → ( ( coeff ‘ Xp ) ‘ 𝐴 ) = if ( 𝐴 = 1 , 1 , 0 ) )

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	⊢ 1 ∈ ℂ
2		1nn0	⊢ 1 ∈ ℕ0
3		mptresid	⊢ ( I ↾ ℂ ) = ( 𝑧 ∈ ℂ ↦ 𝑧 )
4		df-idp	⊢ Xp = ( I ↾ ℂ )
5		exp1	⊢ ( 𝑧 ∈ ℂ → ( 𝑧 ↑ 1 ) = 𝑧 )
6	5	oveq2d	⊢ ( 𝑧 ∈ ℂ → ( 1 · ( 𝑧 ↑ 1 ) ) = ( 1 · 𝑧 ) )
7		mulid2	⊢ ( 𝑧 ∈ ℂ → ( 1 · 𝑧 ) = 𝑧 )
8	6 7	eqtrd	⊢ ( 𝑧 ∈ ℂ → ( 1 · ( 𝑧 ↑ 1 ) ) = 𝑧 )
9	8	mpteq2ia	⊢ ( 𝑧 ∈ ℂ ↦ ( 1 · ( 𝑧 ↑ 1 ) ) ) = ( 𝑧 ∈ ℂ ↦ 𝑧 )
10	3 4 9	3eqtr4i	⊢ Xp = ( 𝑧 ∈ ℂ ↦ ( 1 · ( 𝑧 ↑ 1 ) ) )
11	10	coe1term	⊢ ( ( 1 ∈ ℂ ∧ 1 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ) → ( ( coeff ‘ Xp ) ‘ 𝐴 ) = if ( 𝐴 = 1 , 1 , 0 ) )
12	1 2 11	mp3an12	⊢ ( 𝐴 ∈ ℕ0 → ( ( coeff ‘ Xp ) ‘ 𝐴 ) = if ( 𝐴 = 1 , 1 , 0 ) )