Definition df-0p 25629

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 25628	. 2 class 0𝑝
2		cc 11026	. . 3 class ℂ
3		cc0 11028	. . . 4 class 0
4	3	csn 4579	. . 3 class {0}
5	2, 4	cxp 5621	. 2 class (ℂ × {0})
6	1, 5	wceq 1542	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  25630  0plef  25631  0pledm  25632  itg1ge0  25645  mbfi1fseqlem5  25678  itg2addlem  25717  ply0  26171  coeeulem  26187  dgrnznn  26210  coe0  26219  dgr0  26226  dgreq0  26229  dgrmulc  26235  plymul0or  26246  plydiveu  26264  fta1lem  26273  fta1  26274  quotcan  26275  plyexmo  26279  elqaalem3  26287  aaliou2  26306  plymul02  34682  mpaaeu  43429  sinnpoly  47174