Definition df-0p 23437

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 23436	. 2 class 0𝑝
2		cc 9934	. . 3 class ℂ
3		cc0 9936	. . . 4 class 0
4	3	csn 4177	. . 3 class {0}
5	2, 4	cxp 5112	. 2 class (ℂ × {0})
6	1, 5	wceq 1483	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  23438  0plef  23439  0pledm  23440  itg1ge0  23453  mbfi1fseqlem5  23486  itg2addlem  23525  ply0  23964  coeeulem  23980  dgrnznn  24003  coe0  24012  dgr0  24018  dgreq0  24021  dgrmulc  24027  plymul0or  24036  plydiveu  24053  fta1lem  24062  fta1  24063  quotcan  24064  plyexmo  24068  elqaalem3  24076  aaliou2  24095  plymul02  30623  mpaaeu  37720