This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC TOPOLOGY Metric spaces Normed algebraic structures 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 ‘ 𝑔 ) }