Theorem ngpms 23206

Description: A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)

Assertion

Ref	Expression
ngpms	⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp)

Proof of Theorem ngpms

Step	Hyp	Ref	Expression
1		eqid 2798	. . 3 ⊢ (norm‘𝐺) = (norm‘𝐺)
2		eqid 2798	. . 3 ⊢ (-g‘𝐺) = (-g‘𝐺)
3		eqid 2798	. . 3 ⊢ (dist‘𝐺) = (dist‘𝐺)
4	1, 2, 3	isngp 23202	. 2 ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ((norm‘𝐺) ∘ (-g‘𝐺)) ⊆ (dist‘𝐺)))
5	4	simp2bi 1143	1 ⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp)

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3881   ∘ ccom 5523  ‘cfv 6324  distcds 16566  Grpcgrp 18095  -_gcsg 18097  MetSpcms 22925  normcnm 23183  NrmGrpcngp 23184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-co 5528  df-iota 6283  df-fv 6332  df-ngp 23190

This theorem is referenced by:  ngpxms  23207  ngptps  23208  ngpmet  23209  isngp4  23218  nmmtri  23228  nmrtri  23230  subgngp  23241  ngptgp  23242  tngngp2  23258  nlmvscnlem2  23291  nlmvscnlem1  23292  nlmvscn  23293  nrginvrcn  23298  nghmcn  23351  nmcn  23449  nmhmcn  23725  ipcnlem2  23848  ipcnlem1  23849  ipcn  23850  nglmle  23906  cssbn  23979  minveclem2  24030  minveclem3b  24032  minveclem3  24033  minveclem4  24036  minveclem7  24039