Metamath Proof Explorer

Theorem coeidp

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

Ref Expression
Assertion coeidp 
|- ( A e. NN0 -> ( ( coeff ` Xp ) ` A ) = if ( A = 1 , 1 , 0 ) )

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 1nn0 
 |-  1 e. NN0
3 mptresid 
 |-  ( _I |` CC ) = ( z e. CC |-> z )
4 df-idp 
 |-  Xp = ( _I |` CC )
5 exp1 
 |-  ( z e. CC -> ( z ^ 1 ) = z )
6 5 oveq2d 
 |-  ( z e. CC -> ( 1 x. ( z ^ 1 ) ) = ( 1 x. z ) )
7 mulid2 
 |-  ( z e. CC -> ( 1 x. z ) = z )
8 6 7 eqtrd 
 |-  ( z e. CC -> ( 1 x. ( z ^ 1 ) ) = z )
9 8 mpteq2ia 
 |-  ( z e. CC |-> ( 1 x. ( z ^ 1 ) ) ) = ( z e. CC |-> z )
10 3 4 9 3eqtr4i 
 |-  Xp = ( z e. CC |-> ( 1 x. ( z ^ 1 ) ) )
11 10 coe1term 
 |-  ( ( 1 e. CC /\ 1 e. NN0 /\ A e. NN0 ) -> ( ( coeff ` Xp ) ` A ) = if ( A = 1 , 1 , 0 ) )
12 1 2 11 mp3an12 
 |-  ( A e. NN0 -> ( ( coeff ` Xp ) ` A ) = if ( A = 1 , 1 , 0 ) )