Theorem cnfld0

Description: Zero is the zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014)

	Ref	Expression
Assertion	cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$

Proof

Step	Hyp	Ref	Expression
1		00id	$$⊢0+0=0$$
2		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
3		ringgrp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Grp}$$
4	2 3	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Grp}$$
5		0cn	$$⊢0\in ℂ$$
6		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
7		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
8		eqid	$$⊢0_{{ℂ}_{\mathrm{fld}}}=0_{{ℂ}_{\mathrm{fld}}}$$
9	6 7 8	grpid	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{Grp}\wedge 0\in ℂ\right)\to \left(0+0=0\leftrightarrow 0_{{ℂ}_{\mathrm{fld}}}=0\right)$$
10	4 5 9	mp2an	$$⊢0+0=0\leftrightarrow 0_{{ℂ}_{\mathrm{fld}}}=0$$
11	1 10	mpbi	$$⊢0_{{ℂ}_{\mathrm{fld}}}=0$$
12	11	eqcomi	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$