Definition df-0p 19515

Description: Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014.)

Assertion

Ref	Expression
df-0p	|- 0 p = ( CC X. { 0 } )

Detailed syntax breakdown of Definition df-0p

Step	Hyp	Ref	Expression
1		c0p 19514	. 2 class 0 p
2		cc 8944	. . 3 class CC
3		cc0 8946	. . . 4 class 0
4	3	csn 3774	. . 3 class { 0 }
5	2, 4	cxp 4835	. 2 class ( CC X. { 0 } )
6	1, 5	wceq 1649	1 wff 0 p = ( CC X. { 0 } )

This definition is referenced by:  0pval  19516  0plef  19517  0pledm  19518  itg1ge0  19531  mbfi1fseqlem5  19564  itg2addlem  19603  ply0  20080  coeeulem  20096  coe0  20127  dgr0  20133  dgreq0  20136  dgrmulc  20142  plymul0or  20151  plydiveu  20168  fta1lem  20177  fta1  20178  quotcan  20179  plyexmo  20183  elqaalem3  20191  aaliou2  20210  dgrnznn  27208  mpaaeu  27223