Definition df-ngp

Description: Define a normed group, which is a group with a right-translation-invariant metric. This is not a standard notion, but is helpful as the most general context in which a metric-like norm makes sense. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Assertion	df-ngp	$$⊢\mathrm{NrmGrp}=\left\{g\in \left(\mathrm{Grp}\cap \mathrm{MetSp}\right)|\mathrm{norm}\left(g\right)\circ {-}_g\subseteq \mathrm{dist}\left(g\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cngp	$$class\mathrm{NrmGrp}$$
1		vg	$$setvarg$$
2		cgrp	$$class\mathrm{Grp}$$
3		cms	$$class\mathrm{MetSp}$$
4	2 3	cin	$$class\left(\mathrm{Grp}\cap \mathrm{MetSp}\right)$$
5		cnm	$$class\mathrm{norm}$$
6	1	cv	$$setvarg$$
7	6 5	cfv	$$class\mathrm{norm}\left(g\right)$$
8		csg	$$class{-}_{𝑔}$$
9	6 8	cfv	$$class{-}_g$$
10	7 9	ccom	$$class\left(\mathrm{norm}\left(g\right)\circ {-}_g\right)$$
11		cds	$$class\mathrm{dist}$$
12	6 11	cfv	$$class\mathrm{dist}\left(g\right)$$
13	10 12	wss	$$wff\mathrm{norm}\left(g\right)\circ {-}_g\subseteq \mathrm{dist}\left(g\right)$$
14	13 1 4	crab	$$class\left\{g\in \left(\mathrm{Grp}\cap \mathrm{MetSp}\right)|\mathrm{norm}\left(g\right)\circ {-}_g\subseteq \mathrm{dist}\left(g\right)\right\}$$
15	0 14	wceq	$$wff\mathrm{NrmGrp}=\left\{g\in \left(\mathrm{Grp}\cap \mathrm{MetSp}\right)|\mathrm{norm}\left(g\right)\circ {-}_g\subseteq \mathrm{dist}\left(g\right)\right\}$$