Definition df-ngp 24084

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 24078	. 2 class NrmGrp
2		vg	. . . . . . 7 setvar 𝑔
3	2	cv 1541	. . . . . 6 class 𝑔
4		cnm 24077	. . . . . 6 class norm
5	3, 4	cfv 6541	. . . . 5 class (norm‘𝑔)
6		csg 18818	. . . . . 6 class -g
7	3, 6	cfv 6541	. . . . 5 class (-g‘𝑔)
8	5, 7	ccom 5680	. . . 4 class ((norm‘𝑔) ∘ (-g‘𝑔))
9		cds 17203	. . . . 5 class dist
10	3, 9	cfv 6541	. . . 4 class (dist‘𝑔)
11	8, 10	wss 3948	. . 3 wff ((norm‘𝑔) ∘ (-g‘𝑔)) ⊆ (dist‘𝑔)
12		cgrp 18816	. . . 4 class Grp
13		cms 23816	. . . 4 class MetSp
14	12, 13	cin 3947	. . 3 class (Grp ∩ MetSp)
15	11, 2, 14	crab 3433	. 2 class {𝑔 ∈ (Grp ∩ MetSp) ∣ ((norm‘𝑔) ∘ (-g‘𝑔)) ⊆ (dist‘𝑔)}
16	1, 15	wceq 1542	1 wff NrmGrp = {𝑔 ∈ (Grp ∩ MetSp) ∣ ((norm‘𝑔) ∘ (-g‘𝑔)) ⊆ (dist‘𝑔)}

This definition is referenced by:  isngp  24097