This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-0p

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

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

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