Definition df-0p 23482

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 23481	. 2 class 0𝑝
2		cc 9972	. . 3 class ℂ
3		cc0 9974	. . . 4 class 0
4	3	csn 4210	. . 3 class {0}
5	2, 4	cxp 5141	. 2 class (ℂ × {0})
6	1, 5	wceq 1523	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  23483  0plef  23484  0pledm  23485  itg1ge0  23498  mbfi1fseqlem5  23531  itg2addlem  23570  ply0  24009  coeeulem  24025  dgrnznn  24048  coe0  24057  dgr0  24063  dgreq0  24066  dgrmulc  24072  plymul0or  24081  plydiveu  24098  fta1lem  24107  fta1  24108  quotcan  24109  plyexmo  24113  elqaalem3  24121  aaliou2  24140  plymul02  30751  mpaaeu  38037