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

Definition df-ngp 18122
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 18116 . 2  class NrmGrp
2 vg . . . . . . 7  set  g
32cv 1631 . . . . . 6  class  g
4 cnm 18115 . . . . . 6  class  norm
53, 4cfv 5271 . . . . 5  class  ( norm `  g )
6 csg 14381 . . . . . 6  class  -g
73, 6cfv 5271 . . . . 5  class  ( -g `  g )
85, 7ccom 4709 . . . 4  class  ( (
norm `  g )  o.  ( -g `  g
) )
9 cds 13233 . . . . 5  class  dist
103, 9cfv 5271 . . . 4  class  ( dist `  g )
118, 10wss 3165 . . 3  wff  ( (
norm `  g )  o.  ( -g `  g
) )  C_  ( dist `  g )
12 cgrp 14378 . . . 4  class  Grp
13 cmt 17899 . . . 4  class  MetSp
1412, 13cin 3164 . . 3  class  ( Grp 
i^i  MetSp )
1511, 2, 14crab 2560 . 2  class  { g  e.  ( Grp  i^i  MetSp
)  |  ( (
norm `  g )  o.  ( -g `  g
) )  C_  ( dist `  g ) }
161, 15wceq 1632 1  wff NrmGrp  =  {
g  e.  ( Grp 
i^i  MetSp )  |  ( ( norm `  g
)  o.  ( -g `  g ) )  C_  ( dist `  g ) }
Colors of variables: wff set class
This definition is referenced by:  isngp  18134
  Copyright terms: Public domain W3C validator