Definition df-ngp 23748

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 23742	. 2 class NrmGrp
2		vg	. . . . . . 7 setvar 𝑔
3	2	cv 1538	. . . . . 6 class 𝑔
4		cnm 23741	. . . . . 6 class norm
5	3, 4	cfv 6437	. . . . 5 class (norm‘𝑔)
6		csg 18588	. . . . . 6 class -g
7	3, 6	cfv 6437	. . . . 5 class (-g‘𝑔)
8	5, 7	ccom 5594	. . . 4 class ((norm‘𝑔) ∘ (-g‘𝑔))
9		cds 16980	. . . . 5 class dist
10	3, 9	cfv 6437	. . . 4 class (dist‘𝑔)
11	8, 10	wss 3888	. . 3 wff ((norm‘𝑔) ∘ (-g‘𝑔)) ⊆ (dist‘𝑔)
12		cgrp 18586	. . . 4 class Grp
13		cms 23480	. . . 4 class MetSp
14	12, 13	cin 3887	. . 3 class (Grp ∩ MetSp)
15	11, 2, 14	crab 3069	. 2 class {𝑔 ∈ (Grp ∩ MetSp) ∣ ((norm‘𝑔) ∘ (-g‘𝑔)) ⊆ (dist‘𝑔)}
16	1, 15	wceq 1539	1 wff NrmGrp = {𝑔 ∈ (Grp ∩ MetSp) ∣ ((norm‘𝑔) ∘ (-g‘𝑔)) ⊆ (dist‘𝑔)}

This definition is referenced by:  isngp  23761