Definition df-ngp 24911

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 24905	. 2 class NrmGrp
2		vg	. . . . . . 7 setvar 𝑔
3	2	cv 1568	. . . . . 6 class 𝑔
4		cnm 24904	. . . . . 6 class norm
5	3, 4	cfv 6543	. . . . 5 class (norm‘𝑔)
6		csg 19155	. . . . . 6 class -g
7	3, 6	cfv 6543	. . . . 5 class (-g‘𝑔)
8	5, 7	ccom 5655	. . . 4 class ((norm‘𝑔) ∘ (-g‘𝑔))
9		cds 17446	. . . . 5 class dist
10	3, 9	cfv 6543	. . . 4 class (dist‘𝑔)
11	8, 10	wss 3896	. . 3 wff ((norm‘𝑔) ∘ (-g‘𝑔)) ⊆ (dist‘𝑔)
12		cgrp 19153	. . . 4 class Grp
13		cms 24646	. . . 4 class MetSp
14	12, 13	cin 4088	. . 3 class (Grp ∩ MetSp)
15	11, 2, 14	crab 3412	. 2 class {𝑔 ∈ (Grp ∩ MetSp) ∣ ((norm‘𝑔) ∘ (-g‘𝑔)) ⊆ (dist‘𝑔)}
16	1, 15	wceq 1569	1 wff NrmGrp = {𝑔 ∈ (Grp ∩ MetSp) ∣ ((norm‘𝑔) ∘ (-g‘𝑔)) ⊆ (dist‘𝑔)}

This definition is used by:  isngp  24924