Definition df-0p 25569

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 25568	. 2 class 0𝑝
2		cc 11007	. . 3 class ℂ
3		cc0 11009	. . . 4 class 0
4	3	csn 4577	. . 3 class {0}
5	2, 4	cxp 5617	. 2 class (ℂ × {0})
6	1, 5	wceq 1540	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  25570  0plef  25571  0pledm  25572  itg1ge0  25585  mbfi1fseqlem5  25618  itg2addlem  25657  ply0  26111  coeeulem  26127  dgrnznn  26150  coe0  26159  dgr0  26166  dgreq0  26169  dgrmulc  26175  plymul0or  26186  plydiveu  26204  fta1lem  26213  fta1  26214  quotcan  26215  plyexmo  26219  elqaalem3  26227  aaliou2  26246  plymul02  34530  mpaaeu  43143  sinnpoly  46895