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

Definition df-ngp 21270
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 21264 . 2  class NrmGrp
2 vg . . . . . . 7  setvar  g
32cv 1397 . . . . . 6  class  g
4 cnm 21263 . . . . . 6  class  norm
53, 4cfv 5570 . . . . 5  class  ( norm `  g )
6 csg 16254 . . . . . 6  class  -g
73, 6cfv 5570 . . . . 5  class  ( -g `  g )
85, 7ccom 4992 . . . 4  class  ( (
norm `  g )  o.  ( -g `  g
) )
9 cds 14793 . . . . 5  class  dist
103, 9cfv 5570 . . . 4  class  ( dist `  g )
118, 10wss 3461 . . 3  wff  ( (
norm `  g )  o.  ( -g `  g
) )  C_  ( dist `  g )
12 cgrp 16252 . . . 4  class  Grp
13 cmt 20987 . . . 4  class  MetSp
1412, 13cin 3460 . . 3  class  ( Grp 
i^i  MetSp )
1511, 2, 14crab 2808 . 2  class  { g  e.  ( Grp  i^i  MetSp
)  |  ( (
norm `  g )  o.  ( -g `  g
) )  C_  ( dist `  g ) }
161, 15wceq 1398 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  21282
  Copyright terms: Public domain W3C validator