Definition df-ngp

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)

	Ref	Expression
Assertion	df-ngp	|- NrmGrp = { g e. ( Grp i^i MetSp ) | ( ( norm ` g ) o. ( -g ` g ) ) C_ ( dist ` g ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cngp	|- NrmGrp
1		vg	|- g
2		cgrp	|- Grp
3		cms	|- MetSp
4	2 3	cin	|- ( Grp i^i MetSp )
5		cnm	|- norm
6	1	cv	|- g
7	6 5	cfv	|- ( norm ` g )
8		csg	|- -g
9	6 8	cfv	|- ( -g ` g )
10	7 9	ccom	|- ( ( norm ` g ) o. ( -g ` g ) )
11		cds	|- dist
12	6 11	cfv	|- ( dist ` g )
13	10 12	wss	|- ( ( norm ` g ) o. ( -g ` g ) ) C_ ( dist ` g )
14	13 1 4	crab	|- { g e. ( Grp i^i MetSp ) | ( ( norm ` g ) o. ( -g ` g ) ) C_ ( dist ` g ) }
15	0 14	wceq	|- NrmGrp = { g e. ( Grp i^i MetSp ) | ( ( norm ` g ) o. ( -g ` g ) ) C_ ( dist ` g ) }