Theorem cnmgpid

Description: The group identity element of nonzero complex number multiplication is one. (Contributed by Steve Rodriguez, 23-Feb-2007) (Revised by AV, 26-Aug-2021)

	Ref	Expression
Hypothesis	cnmgpabl.m	$$⊢M={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)$$
Assertion	cnmgpid	$$⊢0_M=1$$

Proof

Step	Hyp	Ref	Expression
1		cnmgpabl.m	$$⊢M={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)$$
2		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
3		difss	$$⊢ℂ\setminus \left\{0\right\}\subseteq ℂ$$
4		ax-1cn	$$⊢1\in ℂ$$
5		ax-1ne0	$$⊢1\ne 0$$
6		eldifsn	$$⊢1\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(1\in ℂ\wedge 1\ne 0\right)$$
7	4 5 6	mpbir2an	$$⊢1\in \left(ℂ\setminus \left\{0\right\}\right)$$
8		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
9		cnfld1	$$⊢1=1_{{ℂ}_{\mathrm{fld}}}$$
10	1 8 9	ringidss	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\wedge ℂ\setminus \left\{0\right\}\subseteq ℂ\wedge 1\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to 1=0_M$$
11	10	eqcomd	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\wedge ℂ\setminus \left\{0\right\}\subseteq ℂ\wedge 1\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to 0_M=1$$
12	2 3 7 11	mp3an	$$⊢0_M=1$$