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 ⊢ A ∈ ℕ 0 → coeff ⁡ X p ⁡ A = if A = 1 1 0

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 1nn0 ⊢ 1 ∈ ℕ 0
3 mptresid ⊢ I ↾ ℂ = z ∈ ℂ ⟼ z
4 df-idp ⊢ X p = I ↾ ℂ
5 exp1 ⊢ z ∈ ℂ → z 1 = z
6 5 oveq2d ⊢ z ∈ ℂ → 1 ⁢ z 1 = 1 ⁢ z
7 mullid ⊢ z ∈ ℂ → 1 ⁢ z = z
8 6 7 eqtrd ⊢ z ∈ ℂ → 1 ⁢ z 1 = z
9 8 mpteq2ia ⊢ z ∈ ℂ ⟼ 1 ⁢ z 1 = z ∈ ℂ ⟼ z
10 3 4 9 3eqtr4i ⊢ X p = z ∈ ℂ ⟼ 1 ⁢ z 1
11 10 coe1term ⊢ 1 ∈ ℂ ∧ 1 ∈ ℕ 0 ∧ A ∈ ℕ 0 → coeff ⁡ X p ⁡ A = if A = 1 1 0
12 1 2 11 mp3an12 ⊢ A ∈ ℕ 0 → coeff ⁡ X p ⁡ A = if A = 1 1 0