Definition df-0p 25605

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 25604	. 2 class 0𝑝
2		cc 11044	. . 3 class ℂ
3		cc0 11046	. . . 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  25606  0plef  25607  0pledm  25608  itg1ge0  25621  mbfi1fseqlem5  25654  itg2addlem  25693  ply0  26147  coeeulem  26163  dgrnznn  26186  coe0  26195  dgr0  26202  dgreq0  26205  dgrmulc  26211  plymul0or  26222  plydiveu  26240  fta1lem  26249  fta1  26250  quotcan  26251  plyexmo  26255  elqaalem3  26263  aaliou2  26282  plymul02  34531  mpaaeu  43133  sinnpoly  46886