Theorem ngpgrp

Description: A normed group is a group. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Assertion	ngpgrp	$$⊢G\in \mathrm{NrmGrp}\to G\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{norm}\left(G\right)=\mathrm{norm}\left(G\right)$$
2		eqid	$$⊢{-}_G={-}_G$$
3		eqid	$$⊢\mathrm{dist}\left(G\right)=\mathrm{dist}\left(G\right)$$
4	1 2 3	isngp	$$⊢G\in \mathrm{NrmGrp}\leftrightarrow \left(G\in \mathrm{Grp}\wedge G\in \mathrm{MetSp}\wedge \mathrm{norm}\left(G\right)\circ {-}_G\subseteq \mathrm{dist}\left(G\right)\right)$$
5	4	simp1bi	$$⊢G\in \mathrm{NrmGrp}\to G\in \mathrm{Grp}$$