Theorem cnngp

Description: The complex numbers form a normed group. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Assertion	cnngp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{NrmGrp}$$

Proof

Step	Hyp	Ref	Expression
1		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
2		ringgrp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Grp}$$
3	1 2	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Grp}$$
4		cnfldms	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{MetSp}$$
5		ssid	$$⊢\mathrm{abs}\circ -\subseteq \mathrm{abs}\circ -$$
6		cnfldnm	$$⊢\mathrm{abs}=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)$$
7		cnfldsub	$$⊢-={-}_{{ℂ}_{\mathrm{fld}}}$$
8		cnfldds	$$⊢\mathrm{abs}\circ -=\mathrm{dist}\left({ℂ}_{\mathrm{fld}}\right)$$
9	6 7 8	isngp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{NrmGrp}\leftrightarrow \left({ℂ}_{\mathrm{fld}}\in \mathrm{Grp}\wedge {ℂ}_{\mathrm{fld}}\in \mathrm{MetSp}\wedge \mathrm{abs}\circ -\subseteq \mathrm{abs}\circ -\right)$$
10	3 4 5 9	mpbir3an	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{NrmGrp}$$