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 ‘ 𝑔 ) }