Definition df-0p 25899

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 25898	. 2 class 0𝑝
2		cc 11125	. . 3 class ℂ
3		cc0 11127	. . . 4 class 0
4	3	csn 4587	. . 3 class {0}
5	2, 4	cxp 5657	. 2 class (ℂ × {0})
6	1, 5	wceq 1570	1 wff 0𝑝 = (ℂ × {0})

This definition is used by:  0pval  25900  0plef  25901  0pledm  25902  itg1ge0  25915  mbfi1fseqlem5  25948  itg2addlem  25987  ply0  26435  coeeulem  26451  dgrnznn  26474  coe0  26483  dgr0  26489  dgreq0  26492  dgrmulc  26498  plymul0or  26509  plymul02  26511  plydiveu  26529  fta1lem  26538  fta1  26539  quotcan  26540  plyexmo  26544  elqaalem3  26552  aaliou2  26573  mpaaeu  43978  sinnpoly  47746