Definition df-0p 25840

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 25839	. 2 class 0𝑝
2		cc 11104	. . 3 class ℂ
3		cc0 11106	. . . 4 class 0
4	3	csn 4588	. . 3 class {0}
5	2, 4	cxp 5658	. 2 class (ℂ × {0})
6	1, 5	wceq 1569	1 wff 0𝑝 = (ℂ × {0})

This definition is used by:  0pval  25841  0plef  25842  0pledm  25843  itg1ge0  25856  mbfi1fseqlem5  25889  itg2addlem  25928  ply0  26376  coeeulem  26392  dgrnznn  26415  coe0  26424  dgr0  26430  dgreq0  26433  dgrmulc  26439  plymul0or  26450  plymul02  26452  plydiveu  26470  fta1lem  26479  fta1  26480  quotcan  26481  plyexmo  26485  elqaalem3  26493  aaliou2  26514  mpaaeu  43905  sinnpoly  47656