Definition df-0p 25598

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 25597	. 2 class 0𝑝
2		cc 11004	. . 3 class ℂ
3		cc0 11006	. . . 4 class 0
4	3	csn 4573	. . 3 class {0}
5	2, 4	cxp 5612	. 2 class (ℂ × {0})
6	1, 5	wceq 1541	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  25599  0plef  25600  0pledm  25601  itg1ge0  25614  mbfi1fseqlem5  25647  itg2addlem  25686  ply0  26140  coeeulem  26156  dgrnznn  26179  coe0  26188  dgr0  26195  dgreq0  26198  dgrmulc  26204  plymul0or  26215  plydiveu  26233  fta1lem  26242  fta1  26243  quotcan  26244  plyexmo  26248  elqaalem3  26256  aaliou2  26275  plymul02  34559  mpaaeu  43242  sinnpoly  46990