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

Definition df-0p 21828
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 21827 . 2  class  0p
2 cc 9489 . . 3  class  CC
3 cc0 9491 . . . 4  class  0
43csn 4027 . . 3  class  { 0 }
52, 4cxp 4997 . 2  class  ( CC 
X.  { 0 } )
61, 5wceq 1379 1  wff  0p  =  ( CC  X.  { 0 } )
Colors of variables: wff setvar class
This definition is referenced by:  0pval  21829  0plef  21830  0pledm  21831  itg1ge0  21844  mbfi1fseqlem5  21877  itg2addlem  21916  ply0  22356  coeeulem  22372  coe0  22403  dgr0  22409  dgreq0  22412  dgrmulc  22418  plymul0or  22427  plydiveu  22444  fta1lem  22453  fta1  22454  quotcan  22455  plyexmo  22459  elqaalem3  22467  aaliou2  22486  plymul02  28159  dgrnznn  30705  mpaaeu  30720
  Copyright terms: Public domain W3C validator