Definition df-ngp 22388

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 = { g e. ( Grp i^i MetSp ) | ( ( norm ` g ) o. ( -g ` g ) ) C_ ( dist ` g ) }

Detailed syntax breakdown of Definition df-ngp

Step	Hyp	Ref	Expression
1		cngp 22382	. 2 class NrmGrp
2		vg	. . . . . . 7 setvar g
3	2	cv 1482	. . . . . 6 class g
4		cnm 22381	. . . . . 6 class norm
5	3, 4	cfv 5888	. . . . 5 class ( norm ` g )
6		csg 17424	. . . . . 6 class -g
7	3, 6	cfv 5888	. . . . 5 class ( -g ` g )
8	5, 7	ccom 5118	. . . 4 class ( ( norm ` g ) o. ( -g ` g ) )
9		cds 15950	. . . . 5 class dist
10	3, 9	cfv 5888	. . . 4 class ( dist ` g )
11	8, 10	wss 3574	. . 3 wff ( ( norm ` g ) o. ( -g ` g ) ) C_ ( dist ` g )
12		cgrp 17422	. . . 4 class Grp
13		cmt 22123	. . . 4 class MetSp
14	12, 13	cin 3573	. . 3 class ( Grp i^i MetSp )
15	11, 2, 14	crab 2916	. 2 class { g e. ( Grp i^i MetSp ) | ( ( norm ` g ) o. ( -g ` g ) ) C_ ( dist ` g ) }
16	1, 15	wceq 1483	1 wff NrmGrp = { g e. ( Grp i^i MetSp ) | ( ( norm ` g ) o. ( -g ` g ) ) C_ ( dist ` g ) }

This definition is referenced by:  isngp  22400