Metamath Proof Explorer


Definition df-ngp

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)

Ref Expression
Assertion df-ngp NrmGrp = { 𝑔 ∈ ( Grp ∩ MetSp ) ∣ ( ( norm ‘ 𝑔 ) ∘ ( -g𝑔 ) ) ⊆ ( dist ‘ 𝑔 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cngp NrmGrp
1 vg 𝑔
2 cgrp Grp
3 cms MetSp
4 2 3 cin ( Grp ∩ MetSp )
5 cnm norm
6 1 cv 𝑔
7 6 5 cfv ( norm ‘ 𝑔 )
8 csg -g
9 6 8 cfv ( -g𝑔 )
10 7 9 ccom ( ( norm ‘ 𝑔 ) ∘ ( -g𝑔 ) )
11 cds dist
12 6 11 cfv ( dist ‘ 𝑔 )
13 10 12 wss ( ( norm ‘ 𝑔 ) ∘ ( -g𝑔 ) ) ⊆ ( dist ‘ 𝑔 )
14 13 1 4 crab { 𝑔 ∈ ( Grp ∩ MetSp ) ∣ ( ( norm ‘ 𝑔 ) ∘ ( -g𝑔 ) ) ⊆ ( dist ‘ 𝑔 ) }
15 0 14 wceq NrmGrp = { 𝑔 ∈ ( Grp ∩ MetSp ) ∣ ( ( norm ‘ 𝑔 ) ∘ ( -g𝑔 ) ) ⊆ ( dist ‘ 𝑔 ) }