MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-0p Unicode version

Definition df-0p 19550
Description: Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014.)
Assertion
Ref Expression
df-0p  |-  0 p  =  ( CC  X.  { 0 } )

Detailed syntax breakdown of Definition df-0p
StepHypRef Expression
1 c0p 19549 . 2  class  0 p
2 cc 8977 . . 3  class  CC
3 cc0 8979 . . . 4  class  0
43csn 3806 . . 3  class  { 0 }
52, 4cxp 4867 . 2  class  ( CC 
X.  { 0 } )
61, 5wceq 1652 1  wff  0 p  =  ( CC  X.  { 0 } )
Colors of variables: wff set class
This definition is referenced by:  0pval  19551  0plef  19552  0pledm  19553  itg1ge0  19566  mbfi1fseqlem5  19599  itg2addlem  19638  ply0  20115  coeeulem  20131  coe0  20162  dgr0  20168  dgreq0  20171  dgrmulc  20177  plymul0or  20186  plydiveu  20203  fta1lem  20212  fta1  20213  quotcan  20214  plyexmo  20218  elqaalem3  20226  aaliou2  20245  dgrnznn  27255  mpaaeu  27270
  Copyright terms: Public domain W3C validator