Definition df-0p 25187

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 25186	. 2 class 0𝑝
2		cc 11108	. . 3 class ℂ
3		cc0 11110	. . . 4 class 0
4	3	csn 4629	. . 3 class {0}
5	2, 4	cxp 5675	. 2 class (ℂ × {0})
6	1, 5	wceq 1542	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  25188  0plef  25189  0pledm  25190  itg1ge0  25203  mbfi1fseqlem5  25237  itg2addlem  25276  ply0  25722  coeeulem  25738  dgrnznn  25761  coe0  25770  dgr0  25776  dgreq0  25779  dgrmulc  25785  plymul0or  25794  plydiveu  25811  fta1lem  25820  fta1  25821  quotcan  25822  plyexmo  25826  elqaalem3  25834  aaliou2  25853  plymul02  33557  mpaaeu  41892