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