Definition df-0p 25411

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 25410	. 2 class 0𝑝
2		cc 11110	. . 3 class ℂ
3		cc0 11112	. . . 4 class 0
4	3	csn 4628	. . 3 class {0}
5	2, 4	cxp 5674	. 2 class (ℂ × {0})
6	1, 5	wceq 1541	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  25412  0plef  25413  0pledm  25414  itg1ge0  25427  mbfi1fseqlem5  25461  itg2addlem  25500  ply0  25946  coeeulem  25962  dgrnznn  25985  coe0  25994  dgr0  26000  dgreq0  26003  dgrmulc  26009  plymul0or  26018  plydiveu  26035  fta1lem  26044  fta1  26045  quotcan  26046  plyexmo  26050  elqaalem3  26058  aaliou2  26077  plymul02  33843  mpaaeu  42194