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 ↾ ℂ )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cidp Xp
1 cid I
2 cc
3 1 2 cres ( I ↾ ℂ )
4 0 3 wceq Xp = ( I ↾ ℂ )