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

Definition df-ngp 22597
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 = {𝑔 ∈ (Grp ∩ MetSp) ∣ ((norm‘𝑔) ∘ (-g𝑔)) ⊆ (dist‘𝑔)}

Detailed syntax breakdown of Definition df-ngp
StepHypRef Expression
1 cngp 22591 . 2 class NrmGrp
2 vg . . . . . . 7 setvar 𝑔
32cv 1636 . . . . . 6 class 𝑔
4 cnm 22590 . . . . . 6 class norm
53, 4cfv 6098 . . . . 5 class (norm‘𝑔)
6 csg 17625 . . . . . 6 class -g
73, 6cfv 6098 . . . . 5 class (-g𝑔)
85, 7ccom 5312 . . . 4 class ((norm‘𝑔) ∘ (-g𝑔))
9 cds 16158 . . . . 5 class dist
103, 9cfv 6098 . . . 4 class (dist‘𝑔)
118, 10wss 3766 . . 3 wff ((norm‘𝑔) ∘ (-g𝑔)) ⊆ (dist‘𝑔)
12 cgrp 17623 . . . 4 class Grp
13 cmt 22332 . . . 4 class MetSp
1412, 13cin 3765 . . 3 class (Grp ∩ MetSp)
1511, 2, 14crab 3099 . 2 class {𝑔 ∈ (Grp ∩ MetSp) ∣ ((norm‘𝑔) ∘ (-g𝑔)) ⊆ (dist‘𝑔)}
161, 15wceq 1637 1 wff NrmGrp = {𝑔 ∈ (Grp ∩ MetSp) ∣ ((norm‘𝑔) ∘ (-g𝑔)) ⊆ (dist‘𝑔)}
Colors of variables: wff setvar class
This definition is referenced by:  isngp  22609
  Copyright terms: Public domain W3C validator