Definition df-0p 25627

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 25626	. 2 class 0𝑝
2		cc 11024	. . 3 class ℂ
3		cc0 11026	. . . 4 class 0
4	3	csn 4580	. . 3 class {0}
5	2, 4	cxp 5622	. 2 class (ℂ × {0})
6	1, 5	wceq 1541	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  25628  0plef  25629  0pledm  25630  itg1ge0  25643  mbfi1fseqlem5  25676  itg2addlem  25715  ply0  26169  coeeulem  26185  dgrnznn  26208  coe0  26217  dgr0  26224  dgreq0  26227  dgrmulc  26233  plymul0or  26244  plydiveu  26262  fta1lem  26271  fta1  26272  quotcan  26273  plyexmo  26277  elqaalem3  26285  aaliou2  26304  plymul02  34703  mpaaeu  43392  sinnpoly  47137