Definition df-0p 25798

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 25797	. 2 class 0𝑝
2		cc 11098	. . 3 class ℂ
3		cc0 11100	. . . 4 class 0
4	3	csn 4592	. . 3 class {0}
5	2, 4	cxp 5660	. 2 class (ℂ × {0})
6	1, 5	wceq 1567	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  25799  0plef  25800  0pledm  25801  itg1ge0  25814  mbfi1fseqlem5  25847  itg2addlem  25886  ply0  26334  coeeulem  26350  dgrnznn  26373  coe0  26382  dgr0  26388  dgreq0  26391  dgrmulc  26397  plymul0or  26408  plymul02  26410  plydiveu  26428  fta1lem  26437  fta1  26438  quotcan  26439  plyexmo  26443  elqaalem3  26451  aaliou2  26470  mpaaeu  43804  sinnpoly  47552