Definition df-0p 25179

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

This definition is referenced by:  0pval  25180  0plef  25181  0pledm  25182  itg1ge0  25195  mbfi1fseqlem5  25229  itg2addlem  25268  ply0  25714  coeeulem  25730  dgrnznn  25753  coe0  25762  dgr0  25768  dgreq0  25771  dgrmulc  25777  plymul0or  25786  plydiveu  25803  fta1lem  25812  fta1  25813  quotcan  25814  plyexmo  25818  elqaalem3  25826  aaliou2  25845  plymul02  33546  mpaaeu  41878