Definition df-0p 24271

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 24270	. 2 class 0𝑝
2		cc 10535	. . 3 class ℂ
3		cc0 10537	. . . 4 class 0
4	3	csn 4567	. . 3 class {0}
5	2, 4	cxp 5553	. 2 class (ℂ × {0})
6	1, 5	wceq 1537	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  24272  0plef  24273  0pledm  24274  itg1ge0  24287  mbfi1fseqlem5  24320  itg2addlem  24359  ply0  24798  coeeulem  24814  dgrnznn  24837  coe0  24846  dgr0  24852  dgreq0  24855  dgrmulc  24861  plymul0or  24870  plydiveu  24887  fta1lem  24896  fta1  24897  quotcan  24898  plyexmo  24902  elqaalem3  24910  aaliou2  24929  plymul02  31816  mpaaeu  39770