Definition df-idp

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

	Ref	Expression
Assertion	df-idp	$$⊢X^p={\mathrm{I}\upharpoonright }_{ℂ}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cidp	$$class{X}^p$$
1		cid	$$class\mathrm{I}$$
2		cc	$$classℂ$$
3	1 2	cres	$$class\left({\mathrm{I}\upharpoonright }_{ℂ}\right)$$
4	0 3	wceq	$$wff{X}^p={\mathrm{I}\upharpoonright }_{ℂ}$$