Definition df-0p 25631

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 25630	. 2 class 0𝑝
2		cc 11028	. . 3 class ℂ
3		cc0 11030	. . . 4 class 0
4	3	csn 4581	. . 3 class {0}
5	2, 4	cxp 5623	. 2 class (ℂ × {0})
6	1, 5	wceq 1542	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  25632  0plef  25633  0pledm  25634  itg1ge0  25647  mbfi1fseqlem5  25680  itg2addlem  25719  ply0  26173  coeeulem  26189  dgrnznn  26212  coe0  26221  dgr0  26228  dgreq0  26231  dgrmulc  26237  plymul0or  26248  plydiveu  26266  fta1lem  26275  fta1  26276  quotcan  26277  plyexmo  26281  elqaalem3  26289  aaliou2  26308  plymul02  34705  mpaaeu  43459  sinnpoly  47204