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

Definition df-ngp 20020
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 20014 . 2  class NrmGrp
2 vg . . . . . . 7  setvar  g
32cv 1363 . . . . . 6  class  g
4 cnm 20013 . . . . . 6  class  norm
53, 4cfv 5408 . . . . 5  class  ( norm `  g )
6 csg 15398 . . . . . 6  class  -g
73, 6cfv 5408 . . . . 5  class  ( -g `  g )
85, 7ccom 4833 . . . 4  class  ( (
norm `  g )  o.  ( -g `  g
) )
9 cds 14232 . . . . 5  class  dist
103, 9cfv 5408 . . . 4  class  ( dist `  g )
118, 10wss 3318 . . 3  wff  ( (
norm `  g )  o.  ( -g `  g
) )  C_  ( dist `  g )
12 cgrp 15395 . . . 4  class  Grp
13 cmt 19737 . . . 4  class  MetSp
1412, 13cin 3317 . . 3  class  ( Grp 
i^i  MetSp )
1511, 2, 14crab 2711 . 2  class  { g  e.  ( Grp  i^i  MetSp
)  |  ( (
norm `  g )  o.  ( -g `  g
) )  C_  ( dist `  g ) }
161, 15wceq 1364 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  20032
  Copyright terms: Public domain W3C validator