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

Definition df-0p 21123
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 21122 . 2  class  0p
2 cc 9272 . . 3  class  CC
3 cc0 9274 . . . 4  class  0
43csn 3872 . . 3  class  { 0 }
52, 4cxp 4833 . 2  class  ( CC 
X.  { 0 } )
61, 5wceq 1369 1  wff  0p  =  ( CC  X.  { 0 } )
Colors of variables: wff setvar class
This definition is referenced by:  0pval  21124  0plef  21125  0pledm  21126  itg1ge0  21139  mbfi1fseqlem5  21172  itg2addlem  21211  ply0  21651  coeeulem  21667  coe0  21698  dgr0  21704  dgreq0  21707  dgrmulc  21713  plymul0or  21722  plydiveu  21739  fta1lem  21748  fta1  21749  quotcan  21750  plyexmo  21754  elqaalem3  21762  aaliou2  21781  plymul02  26899  dgrnznn  29445  mpaaeu  29460
  Copyright terms: Public domain W3C validator