This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-idp

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

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

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