Definition df-0p 25578

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 25577	. 2 class 0𝑝
2		cc 11073	. . 3 class ℂ
3		cc0 11075	. . . 4 class 0
4	3	csn 4592	. . 3 class {0}
5	2, 4	cxp 5639	. 2 class (ℂ × {0})
6	1, 5	wceq 1540	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  25579  0plef  25580  0pledm  25581  itg1ge0  25594  mbfi1fseqlem5  25627  itg2addlem  25666  ply0  26120  coeeulem  26136  dgrnznn  26159  coe0  26168  dgr0  26175  dgreq0  26178  dgrmulc  26184  plymul0or  26195  plydiveu  26213  fta1lem  26222  fta1  26223  quotcan  26224  plyexmo  26228  elqaalem3  26236  aaliou2  26255  plymul02  34544  mpaaeu  43146