Definition df-0p 25659

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 25658	. 2 class 0𝑝
2		cc 11031	. . 3 class ℂ
3		cc0 11033	. . . 4 class 0
4	3	csn 4558	. . 3 class {0}
5	2, 4	cxp 5619	. 2 class (ℂ × {0})
6	1, 5	wceq 1548	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  25660  0plef  25661  0pledm  25662  itg1ge0  25675  mbfi1fseqlem5  25708  itg2addlem  25747  ply0  26195  coeeulem  26211  dgrnznn  26234  coe0  26243  dgr0  26249  dgreq0  26252  dgrmulc  26258  plymul0or  26269  plydiveu  26286  fta1lem  26295  fta1  26296  quotcan  26297  plyexmo  26301  elqaalem3  26309  aaliou2  26328  plymul02  34742  mpaaeu  43610  sinnpoly  47368