Definition df-0p 25724

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 25723	. 2 class 0𝑝
2		cc 11182	. . 3 class ℂ
3		cc0 11184	. . . 4 class 0
4	3	csn 4648	. . 3 class {0}
5	2, 4	cxp 5698	. 2 class (ℂ × {0})
6	1, 5	wceq 1537	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  25725  0plef  25726  0pledm  25727  itg1ge0  25740  mbfi1fseqlem5  25774  itg2addlem  25813  ply0  26267  coeeulem  26283  dgrnznn  26306  coe0  26315  dgr0  26322  dgreq0  26325  dgrmulc  26331  plymul0or  26340  plydiveu  26358  fta1lem  26367  fta1  26368  quotcan  26369  plyexmo  26373  elqaalem3  26381  aaliou2  26400  plymul02  34523  mpaaeu  43107