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

Definition df-0p 22203
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 22202 . 2  class  0p
2 cc 9507 . . 3  class  CC
3 cc0 9509 . . . 4  class  0
43csn 4032 . . 3  class  { 0 }
52, 4cxp 5006 . 2  class  ( CC 
X.  { 0 } )
61, 5wceq 1395 1  wff  0p  =  ( CC  X.  { 0 } )
Colors of variables: wff setvar class
This definition is referenced by:  0pval  22204  0plef  22205  0pledm  22206  itg1ge0  22219  mbfi1fseqlem5  22252  itg2addlem  22291  ply0  22731  coeeulem  22747  dgrnznn  22770  coe0  22779  dgr0  22785  dgreq0  22788  dgrmulc  22794  plymul0or  22803  plydiveu  22820  fta1lem  22829  fta1  22830  quotcan  22831  plyexmo  22835  elqaalem3  22843  aaliou2  22862  plymul02  28700  mpaaeu  31303
  Copyright terms: Public domain W3C validator