Definition df-0p 25713

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 25712	. 2 class 0𝑝
2		cc 11163	. . 3 class ℂ
3		cc0 11165	. . . 4 class 0
4	3	csn 4636	. . 3 class {0}
5	2, 4	cxp 5684	. 2 class (ℂ × {0})
6	1, 5	wceq 1534	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  25714  0plef  25715  0pledm  25716  itg1ge0  25729  mbfi1fseqlem5  25763  itg2addlem  25802  ply0  26258  coeeulem  26274  dgrnznn  26297  coe0  26306  dgr0  26313  dgreq0  26316  dgrmulc  26322  plymul0or  26331  plydiveu  26349  fta1lem  26358  fta1  26359  quotcan  26360  plyexmo  26364  elqaalem3  26372  aaliou2  26391  plymul02  34430  mpaaeu  42882