Metamath Proof Explorer

Definition df-0p

Description: Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014)

Ref Expression
Assertion df-0p 
|- 0p = ( CC X. { 0 } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 c0p 
 |-  0p
1 cc 
 |-  CC
2 cc0 
 |-  0
3 2 csn 
 |-  { 0 }
4 1 3 cxp 
 |-  ( CC X. { 0 } )
5 0 4 wceq 
 |-  0p = ( CC X. { 0 } )