Definition df-0p 25637

Description: Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014.)

Assertion

Ref	Expression
df-0p	⊢ 0𝑝 = (ℂ × {0})

Detailed syntax breakdown of Definition df-0p

Step	Hyp	Ref	Expression
1		c0p 25636	. 2 class 0𝑝
2		cc 11036	. . 3 class ℂ
3		cc0 11038	. . . 4 class 0
4	3	csn 4567	. . 3 class {0}
5	2, 4	cxp 5629	. 2 class (ℂ × {0})
6	1, 5	wceq 1542	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  25638  0plef  25639  0pledm  25640  itg1ge0  25653  mbfi1fseqlem5  25686  itg2addlem  25725  ply0  26173  coeeulem  26189  dgrnznn  26212  coe0  26221  dgr0  26227  dgreq0  26230  dgrmulc  26236  plymul0or  26247  plydiveu  26264  fta1lem  26273  fta1  26274  quotcan  26275  plyexmo  26279  elqaalem3  26287  aaliou2  26306  plymul02  34690  mpaaeu  43578  sinnpoly  47339