Definition df-0p 25734

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 25733	. 2 class 0𝑝
2		cc 11073	. . 3 class ℂ
3		cc0 11075	. . . 4 class 0
4	3	csn 4584	. . 3 class {0}
5	2, 4	cxp 5647	. 2 class (ℂ × {0})
6	1, 5	wceq 1562	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  25735  0plef  25736  0pledm  25737  itg1ge0  25750  mbfi1fseqlem5  25783  itg2addlem  25822  ply0  26270  coeeulem  26286  dgrnznn  26309  coe0  26318  dgr0  26324  dgreq0  26327  dgrmulc  26333  plymul0or  26344  plymul02  26346  plydiveu  26364  fta1lem  26373  fta1  26374  quotcan  26375  plyexmo  26379  elqaalem3  26387  aaliou2  26406  mpaaeu  43732  sinnpoly  47490