This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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