Metamath Proof Explorer

Definition df-idp

Description: Define the identity polynomial. (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Assertion df-idp 
|- Xp = ( _I |` CC )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cidp 
 |-  Xp
1 cid 
 |-  _I
2 cc 
 |-  CC
3 1 2 cres 
 |-  ( _I |` CC )
4 0 3 wceq 
 |-  Xp = ( _I |` CC )