Database
BASIC TOPOLOGY
Metric spaces
Normed algebraic structures
df-ngp
Metamath Proof Explorer
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 ) }