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	$⊢ NrmGrp = \{g \in (Grp \cap MetSp) \| norm (g) \circ -_{g} \subseteq dist (g)\}$

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-ngp

Detailed syntax breakdown