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

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

Detailed syntax breakdown of Definition df-0p
StepHypRef Expression
1 c0p 21283 . 2  class  0p
2 cc 9394 . . 3  class  CC
3 cc0 9396 . . . 4  class  0
43csn 3988 . . 3  class  { 0 }
52, 4cxp 4949 . 2  class  ( CC 
X.  { 0 } )
61, 5wceq 1370 1  wff  0p  =  ( CC  X.  { 0 } )
Colors of variables: wff setvar class
This definition is referenced by:  0pval  21285  0plef  21286  0pledm  21287  itg1ge0  21300  mbfi1fseqlem5  21333  itg2addlem  21372  ply0  21812  coeeulem  21828  coe0  21859  dgr0  21865  dgreq0  21868  dgrmulc  21874  plymul0or  21883  plydiveu  21900  fta1lem  21909  fta1  21910  quotcan  21911  plyexmo  21915  elqaalem3  21923  aaliou2  21942  plymul02  27111  dgrnznn  29660  mpaaeu  29675
  Copyright terms: Public domain W3C validator