Definition df-0p

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

	Ref	Expression
Assertion	df-0p	$$⊢0_{𝑝}=ℂ\times \left\{0\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c0p	$$class{0}_{𝑝}$$
1		cc	$$classℂ$$
2		cc0	$$class0$$
3	2	csn	$$class\left\{0\right\}$$
4	1 3	cxp	$$class\left(ℂ\times \left\{0\right\}\right)$$
5	0 4	wceq	$$wff{0}_{𝑝}=ℂ\times \left\{0\right\}$$