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

Definition df-0p 19422
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 19421 . 2  class  0 p
2 cc 8914 . . 3  class  CC
3 cc0 8916 . . . 4  class  0
43csn 3750 . . 3  class  { 0 }
52, 4cxp 4809 . 2  class  ( CC 
X.  { 0 } )
61, 5wceq 1649 1  wff  0 p  =  ( CC  X.  { 0 } )
Colors of variables: wff set class
This definition is referenced by:  0pval  19423  0plef  19424  0pledm  19425  itg1ge0  19438  mbfi1fseqlem5  19471  itg2addlem  19510  ply0  19987  coeeulem  20003  coe0  20034  dgr0  20040  dgreq0  20043  dgrmulc  20049  plymul0or  20058  plydiveu  20075  fta1lem  20084  fta1  20085  quotcan  20086  plyexmo  20090  elqaalem3  20098  aaliou2  20117  dgrnznn  27002  mpaaeu  27017
  Copyright terms: Public domain W3C validator