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

Definition df-0p 22505
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 22504 . 2  class  0p
2 cc 9536 . . 3  class  CC
3 cc0 9538 . . . 4  class  0
43csn 4002 . . 3  class  { 0 }
52, 4cxp 4852 . 2  class  ( CC 
X.  { 0 } )
61, 5wceq 1437 1  wff  0p  =  ( CC  X.  { 0 } )
Colors of variables: wff setvar class
This definition is referenced by:  0pval  22506  0plef  22507  0pledm  22508  itg1ge0  22521  mbfi1fseqlem5  22554  itg2addlem  22593  ply0  23030  coeeulem  23046  dgrnznn  23069  coe0  23078  dgr0  23084  dgreq0  23087  dgrmulc  23093  plymul0or  23102  plydiveu  23119  fta1lem  23128  fta1  23129  quotcan  23130  plyexmo  23134  elqaalem3  23142  aaliou2  23161  plymul02  29223  mpaaeu  35714
  Copyright terms: Public domain W3C validator