Definition df-0p 25718

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 25717	. 2 class 0𝑝
2		cc 11150	. . 3 class ℂ
3		cc0 11152	. . . 4 class 0
4	3	csn 4630	. . 3 class {0}
5	2, 4	cxp 5686	. 2 class (ℂ × {0})
6	1, 5	wceq 1536	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  25719  0plef  25720  0pledm  25721  itg1ge0  25734  mbfi1fseqlem5  25768  itg2addlem  25807  ply0  26261  coeeulem  26277  dgrnznn  26300  coe0  26309  dgr0  26316  dgreq0  26319  dgrmulc  26325  plymul0or  26336  plydiveu  26354  fta1lem  26363  fta1  26364  quotcan  26365  plyexmo  26369  elqaalem3  26377  aaliou2  26396  plymul02  34539  mpaaeu  43138