Definition df-0p 25938

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 25937	. 2 class 0𝑝
2		cc 11155	. . 3 class ℂ
3		cc0 11157	. . . 4 class 0
4	3	csn 4584	. . 3 class {0}
5	2, 4	cxp 5646	. 2 class (ℂ × {0})
6	1, 5	wceq 1570	1 wff 0𝑝 = (ℂ × {0})

This definition is used by:  0pval  25939  0plef  25940  0pledm  25941  itg1ge0  25954  mbfi1fseqlem5  25987  itg2addlem  26026  ply0  26473  coeeulem  26490  dgrnznn  26513  coe0  26522  dgr0  26528  dgreq0  26531  dgrmulc  26537  plymul0or  26548  plymul02  26550  plydiveu  26568  fta1lem  26577  fta1  26578  quotcan  26581  plyexmo  26585  elqaalem3  26593  aaliou2  26616  mpaaeu  44089  sinnpoly  47857