Definition df-0p 25651

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 25650	. 2 class 0𝑝
2		cc 11031	. . 3 class ℂ
3		cc0 11033	. . . 4 class 0
4	3	csn 4568	. . 3 class {0}
5	2, 4	cxp 5624	. 2 class (ℂ × {0})
6	1, 5	wceq 1542	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  25652  0plef  25653  0pledm  25654  itg1ge0  25667  mbfi1fseqlem5  25700  itg2addlem  25739  ply0  26187  coeeulem  26203  dgrnznn  26226  coe0  26235  dgr0  26241  dgreq0  26244  dgrmulc  26250  plymul0or  26261  plydiveu  26279  fta1lem  26288  fta1  26289  quotcan  26290  plyexmo  26294  elqaalem3  26302  aaliou2  26321  plymul02  34710  mpaaeu  43602  sinnpoly  47357