Metamath Proof Explorer

Theorem dgrid

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

Ref Expression
Assertion dgrid 
|- ( deg ` Xp ) = 1

Proof

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