Definition df-ngp 24791

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 24785	. 2 class NrmGrp
2		vg	. . . . . . 7 setvar 𝑔
3	2	cv 1569	. . . . . 6 class 𝑔
4		cnm 24784	. . . . . 6 class norm
5	3, 4	cfv 6540	. . . . 5 class (norm‘𝑔)
6		csg 19046	. . . . . 6 class -g
7	3, 6	cfv 6540	. . . . 5 class (-g‘𝑔)
8	5, 7	ccom 5667	. . . 4 class ((norm‘𝑔) ∘ (-g‘𝑔))
9		cds 17341	. . . . 5 class dist
10	3, 9	cfv 6540	. . . 4 class (dist‘𝑔)
11	8, 10	wss 3906	. . 3 wff ((norm‘𝑔) ∘ (-g‘𝑔)) ⊆ (dist‘𝑔)
12		cgrp 19044	. . . 4 class Grp
13		cms 24526	. . . 4 class MetSp
14	12, 13	cin 3905	. . 3 class (Grp ∩ MetSp)
15	11, 2, 14	crab 3418	. 2 class {𝑔 ∈ (Grp ∩ MetSp) ∣ ((norm‘𝑔) ∘ (-g‘𝑔)) ⊆ (dist‘𝑔)}
16	1, 15	wceq 1570	1 wff NrmGrp = {𝑔 ∈ (Grp ∩ MetSp) ∣ ((norm‘𝑔) ∘ (-g‘𝑔)) ⊆ (dist‘𝑔)}

This definition is used by:  isngp  24804