Definition df-0p 23958

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 23957	. 2 class 0𝑝
2		cc 10388	. . 3 class ℂ
3		cc0 10390	. . . 4 class 0
4	3	csn 4478	. . 3 class {0}
5	2, 4	cxp 5448	. 2 class (ℂ × {0})
6	1, 5	wceq 1525	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  23959  0plef  23960  0pledm  23961  itg1ge0  23974  mbfi1fseqlem5  24007  itg2addlem  24046  ply0  24485  coeeulem  24501  dgrnznn  24524  coe0  24533  dgr0  24539  dgreq0  24542  dgrmulc  24548  plymul0or  24557  plydiveu  24574  fta1lem  24583  fta1  24584  quotcan  24585  plyexmo  24589  elqaalem3  24597  aaliou2  24616  plymul02  31429  mpaaeu  39256