Definition df-0p 25705

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 25704	. 2 class 0𝑝
2		cc 11153	. . 3 class ℂ
3		cc0 11155	. . . 4 class 0
4	3	csn 4626	. . 3 class {0}
5	2, 4	cxp 5683	. 2 class (ℂ × {0})
6	1, 5	wceq 1540	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  25706  0plef  25707  0pledm  25708  itg1ge0  25721  mbfi1fseqlem5  25754  itg2addlem  25793  ply0  26247  coeeulem  26263  dgrnznn  26286  coe0  26295  dgr0  26302  dgreq0  26305  dgrmulc  26311  plymul0or  26322  plydiveu  26340  fta1lem  26349  fta1  26350  quotcan  26351  plyexmo  26355  elqaalem3  26363  aaliou2  26382  plymul02  34561  mpaaeu  43162