Definition df-0p 26018

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 26017	. 2 class 0𝑝
2		cc 11222	. . 3 class ℂ
3		cc0 11224	. . . 4 class 0
4	3	csn 4588	. . 3 class {0}
5	2, 4	cxp 5653	. 2 class (ℂ × {0})
6	1, 5	wceq 1570	1 wff 0𝑝 = (ℂ × {0})

This definition is used by:  0pval  26019  0plef  26020  0pledm  26021  itg1ge0  26034  mbfi1fseqlem5  26067  itg2addlem  26106  ply0  26553  coeeulem  26570  dgrnznn  26593  coe0  26602  dgr0  26608  dgreq0  26611  dgrmulc  26617  plymul0or  26626  plymul02  26628  plydiveu  26646  fta1lem  26655  fta1  26656  quotcan  26659  plyexmo  26663  elqaalem3  26671  aaliou2  26694  mpaaeu  44342  sinnpoly  48144