Definition df-0p 24371

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 24370	. 2 class 0𝑝
2		cc 10574	. . 3 class ℂ
3		cc0 10576	. . . 4 class 0
4	3	csn 4523	. . 3 class {0}
5	2, 4	cxp 5523	. 2 class (ℂ × {0})
6	1, 5	wceq 1539	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  24372  0plef  24373  0pledm  24374  itg1ge0  24387  mbfi1fseqlem5  24420  itg2addlem  24459  ply0  24905  coeeulem  24921  dgrnznn  24944  coe0  24953  dgr0  24959  dgreq0  24962  dgrmulc  24968  plymul0or  24977  plydiveu  24994  fta1lem  25003  fta1  25004  quotcan  25005  plyexmo  25009  elqaalem3  25017  aaliou2  25036  plymul02  32045  mpaaeu  40468