Definition df-0p 24739

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 24738	. 2 class 0𝑝
2		cc 10800	. . 3 class ℂ
3		cc0 10802	. . . 4 class 0
4	3	csn 4558	. . 3 class {0}
5	2, 4	cxp 5578	. 2 class (ℂ × {0})
6	1, 5	wceq 1539	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  24740  0plef  24741  0pledm  24742  itg1ge0  24755  mbfi1fseqlem5  24789  itg2addlem  24828  ply0  25274  coeeulem  25290  dgrnznn  25313  coe0  25322  dgr0  25328  dgreq0  25331  dgrmulc  25337  plymul0or  25346  plydiveu  25363  fta1lem  25372  fta1  25373  quotcan  25374  plyexmo  25378  elqaalem3  25386  aaliou2  25405  plymul02  32425  mpaaeu  40891