Definition df-0p 25571

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 25570	. 2 class 0𝑝
2		cc 11066	. . 3 class ℂ
3		cc0 11068	. . . 4 class 0
4	3	csn 4589	. . 3 class {0}
5	2, 4	cxp 5636	. 2 class (ℂ × {0})
6	1, 5	wceq 1540	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  25572  0plef  25573  0pledm  25574  itg1ge0  25587  mbfi1fseqlem5  25620  itg2addlem  25659  ply0  26113  coeeulem  26129  dgrnznn  26152  coe0  26161  dgr0  26168  dgreq0  26171  dgrmulc  26177  plymul0or  26188  plydiveu  26206  fta1lem  26215  fta1  26216  quotcan  26217  plyexmo  26221  elqaalem3  26229  aaliou2  26248  plymul02  34537  mpaaeu  43139  sinnpoly  46892