Theorem isngp

Description: The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	isngp.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
	isngp.z	⊢ − = ( -g ‘ 𝐺 )
	isngp.d	⊢ 𝐷 = ( dist ‘ 𝐺 )
Assertion	isngp	⊢ ( 𝐺 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		isngp.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
2		isngp.z	⊢ − = ( -g ‘ 𝐺 )
3		isngp.d	⊢ 𝐷 = ( dist ‘ 𝐺 )
4		elin	⊢ ( 𝐺 ∈ ( Grp ∩ MetSp ) ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) )
5	4	anbi1i	⊢ ( ( 𝐺 ∈ ( Grp ∩ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) )
6		fveq2	⊢ ( 𝑔 = 𝐺 → ( norm ‘ 𝑔 ) = ( norm ‘ 𝐺 ) )
7	6 1	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( norm ‘ 𝑔 ) = 𝑁 )
8		fveq2	⊢ ( 𝑔 = 𝐺 → ( -g ‘ 𝑔 ) = ( -g ‘ 𝐺 ) )
9	8 2	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( -g ‘ 𝑔 ) = − )
10	7 9	coeq12d	⊢ ( 𝑔 = 𝐺 → ( ( norm ‘ 𝑔 ) ∘ ( -g ‘ 𝑔 ) ) = ( 𝑁 ∘ − ) )
11		fveq2	⊢ ( 𝑔 = 𝐺 → ( dist ‘ 𝑔 ) = ( dist ‘ 𝐺 ) )
12	11 3	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( dist ‘ 𝑔 ) = 𝐷 )
13	10 12	sseq12d	⊢ ( 𝑔 = 𝐺 → ( ( ( norm ‘ 𝑔 ) ∘ ( -g ‘ 𝑔 ) ) ⊆ ( dist ‘ 𝑔 ) ↔ ( 𝑁 ∘ − ) ⊆ 𝐷 ) )
14		df-ngp	⊢ NrmGrp = { 𝑔 ∈ ( Grp ∩ MetSp ) ∣ ( ( norm ‘ 𝑔 ) ∘ ( -g ‘ 𝑔 ) ) ⊆ ( dist ‘ 𝑔 ) }
15	13 14	elrab2	⊢ ( 𝐺 ∈ NrmGrp ↔ ( 𝐺 ∈ ( Grp ∩ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) )
16		df-3an	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) )
17	5 15 16	3bitr4i	⊢ ( 𝐺 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) )