Definition df-ngp 23192

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.)

Assertion

Ref	Expression
df-ngp	⊢ NrmGrp = {𝑔 ∈ (Grp ∩ MetSp) ∣ ((norm‘𝑔) ∘ (-g‘𝑔)) ⊆ (dist‘𝑔)}

Detailed syntax breakdown of Definition df-ngp

Step	Hyp	Ref	Expression
1		cngp 23186	. 2 class NrmGrp
2		vg	. . . . . . 7 setvar 𝑔
3	2	cv 1532	. . . . . 6 class 𝑔
4		cnm 23185	. . . . . 6 class norm
5	3, 4	cfv 6354	. . . . 5 class (norm‘𝑔)
6		csg 18104	. . . . . 6 class -g
7	3, 6	cfv 6354	. . . . 5 class (-g‘𝑔)
8	5, 7	ccom 5558	. . . 4 class ((norm‘𝑔) ∘ (-g‘𝑔))
9		cds 16573	. . . . 5 class dist
10	3, 9	cfv 6354	. . . 4 class (dist‘𝑔)
11	8, 10	wss 3935	. . 3 wff ((norm‘𝑔) ∘ (-g‘𝑔)) ⊆ (dist‘𝑔)
12		cgrp 18102	. . . 4 class Grp
13		cms 22927	. . . 4 class MetSp
14	12, 13	cin 3934	. . 3 class (Grp ∩ MetSp)
15	11, 2, 14	crab 3142	. 2 class {𝑔 ∈ (Grp ∩ MetSp) ∣ ((norm‘𝑔) ∘ (-g‘𝑔)) ⊆ (dist‘𝑔)}
16	1, 15	wceq 1533	1 wff NrmGrp = {𝑔 ∈ (Grp ∩ MetSp) ∣ ((norm‘𝑔) ∘ (-g‘𝑔)) ⊆ (dist‘𝑔)}

This definition is referenced by:  isngp  23204