This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 mullid ⊢ ( 𝑧 ∈ ℂ → ( 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 ) )