MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ngp Structured version   Unicode version

Definition df-ngp 20179
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
StepHypRef Expression
1 cngp 20173 . 2  class NrmGrp
2 vg . . . . . . 7  setvar  g
32cv 1368 . . . . . 6  class  g
4 cnm 20172 . . . . . 6  class  norm
53, 4cfv 5421 . . . . 5  class  ( norm `  g )
6 csg 15416 . . . . . 6  class  -g
73, 6cfv 5421 . . . . 5  class  ( -g `  g )
85, 7ccom 4847 . . . 4  class  ( (
norm `  g )  o.  ( -g `  g
) )
9 cds 14250 . . . . 5  class  dist
103, 9cfv 5421 . . . 4  class  ( dist `  g )
118, 10wss 3331 . . 3  wff  ( (
norm `  g )  o.  ( -g `  g
) )  C_  ( dist `  g )
12 cgrp 15413 . . . 4  class  Grp
13 cmt 19896 . . . 4  class  MetSp
1412, 13cin 3330 . . 3  class  ( Grp 
i^i  MetSp )
1511, 2, 14crab 2722 . 2  class  { g  e.  ( Grp  i^i  MetSp
)  |  ( (
norm `  g )  o.  ( -g `  g
) )  C_  ( dist `  g ) }
161, 15wceq 1369 1  wff NrmGrp  =  {
g  e.  ( Grp 
i^i  MetSp )  |  ( ( norm `  g
)  o.  ( -g `  g ) )  C_  ( dist `  g ) }
Colors of variables: wff setvar class
This definition is referenced by:  isngp  20191
  Copyright terms: Public domain W3C validator