Description: Define the identity polynomial. (Contributed by Mario Carneiro, 17-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | df-idp | |- Xp = ( _I |` CC ) |
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 ) |