Metamath Proof Explorer


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 ) }