Definition df-0p 25644

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 25643	. 2 class 0𝑝
2		cc 11038	. . 3 class ℂ
3		cc0 11040	. . . 4 class 0
4	3	csn 4582	. . 3 class {0}
5	2, 4	cxp 5632	. 2 class (ℂ × {0})
6	1, 5	wceq 1542	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  25645  0plef  25646  0pledm  25647  itg1ge0  25660  mbfi1fseqlem5  25693  itg2addlem  25732  ply0  26186  coeeulem  26202  dgrnznn  26225  coe0  26234  dgr0  26241  dgreq0  26244  dgrmulc  26250  plymul0or  26261  plydiveu  26279  fta1lem  26288  fta1  26289  quotcan  26290  plyexmo  26294  elqaalem3  26302  aaliou2  26321  plymul02  34730  mpaaeu  43536  sinnpoly  47280