Definition df-0p 25991

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 25990	. 2 class 0𝑝
2		cc 11198	. . 3 class ℂ
3		cc0 11200	. . . 4 class 0
4	3	csn 4583	. . 3 class {0}
5	2, 4	cxp 5648	. 2 class (ℂ × {0})
6	1, 5	wceq 1569	1 wff 0𝑝 = (ℂ × {0})

This definition is used by:  0pval  25992  0plef  25993  0pledm  25994  itg1ge0  26007  mbfi1fseqlem5  26040  itg2addlem  26079  ply0  26526  coeeulem  26543  dgrnznn  26566  coe0  26575  dgr0  26581  dgreq0  26584  dgrmulc  26590  plymul0or  26599  plymul02  26601  plydiveu  26619  fta1lem  26628  fta1  26629  quotcan  26632  plyexmo  26636  elqaalem3  26644  aaliou2  26667  mpaaeu  44152  sinnpoly  47941