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

Definition df-0p 22677
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 22676 . 2  class  0p
2 cc 9563 . . 3  class  CC
3 cc0 9565 . . . 4  class  0
43csn 3980 . . 3  class  { 0 }
52, 4cxp 4851 . 2  class  ( CC 
X.  { 0 } )
61, 5wceq 1455 1  wff  0p  =  ( CC  X.  { 0 } )
Colors of variables: wff setvar class
This definition is referenced by:  0pval  22678  0plef  22679  0pledm  22680  itg1ge0  22693  mbfi1fseqlem5  22726  itg2addlem  22765  ply0  23211  coeeulem  23227  dgrnznn  23250  coe0  23259  dgr0  23265  dgreq0  23268  dgrmulc  23274  plymul0or  23283  plydiveu  23300  fta1lem  23309  fta1  23310  quotcan  23311  plyexmo  23315  elqaalem3  23323  elqaalem3OLD  23326  aaliou2  23345  plymul02  29484  mpaaeu  36061
  Copyright terms: Public domain W3C validator