Definition df-0p 25604

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 25603	. 2 class 0𝑝
2		cc 11042	. . 3 class ℂ
3		cc0 11044	. . . 4 class 0
4	3	csn 4585	. . 3 class {0}
5	2, 4	cxp 5629	. 2 class (ℂ × {0})
6	1, 5	wceq 1540	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  25605  0plef  25606  0pledm  25607  itg1ge0  25620  mbfi1fseqlem5  25653  itg2addlem  25692  ply0  26146  coeeulem  26162  dgrnznn  26185  coe0  26194  dgr0  26201  dgreq0  26204  dgrmulc  26210  plymul0or  26221  plydiveu  26239  fta1lem  26248  fta1  26249  quotcan  26250  plyexmo  26254  elqaalem3  26262  aaliou2  26281  plymul02  34530  mpaaeu  43132  sinnpoly  46885