Definition df-0p 25621

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 25620	. 2 class 0𝑝
2		cc 11125	. . 3 class ℂ
3		cc0 11127	. . . 4 class 0
4	3	csn 4601	. . 3 class {0}
5	2, 4	cxp 5652	. 2 class (ℂ × {0})
6	1, 5	wceq 1540	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  25622  0plef  25623  0pledm  25624  itg1ge0  25637  mbfi1fseqlem5  25670  itg2addlem  25709  ply0  26163  coeeulem  26179  dgrnznn  26202  coe0  26211  dgr0  26218  dgreq0  26221  dgrmulc  26227  plymul0or  26238  plydiveu  26256  fta1lem  26265  fta1  26266  quotcan  26267  plyexmo  26271  elqaalem3  26279  aaliou2  26298  plymul02  34524  mpaaeu  43121