Theorem ngpms 24549

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 2737	. . 3 ⊢ (norm‘𝐺) = (norm‘𝐺)
2		eqid 2737	. . 3 ⊢ (-g‘𝐺) = (-g‘𝐺)
3		eqid 2737	. . 3 ⊢ (dist‘𝐺) = (dist‘𝐺)
4	1, 2, 3	isngp 24545	. 2 ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ((norm‘𝐺) ∘ (-g‘𝐺)) ⊆ (dist‘𝐺)))
5	4	simp2bi 1147	1 ⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp)

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3902   ∘ ccom 5629  ‘cfv 6493  distcds 17191  Grpcgrp 18868  -_gcsg 18870  MetSpcms 24267  normcnm 24525  NrmGrpcngp 24526

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-co 5634  df-iota 6449  df-fv 6501  df-ngp 24532

This theorem is referenced by:  ngpxms  24550  ngptps  24551  ngpmet  24552  isngp4  24561  nmmtri  24571  nmrtri  24573  subgngp  24584  ngptgp  24585  tngngp2  24601  nlmvscnlem2  24634  nlmvscnlem1  24635  nlmvscn  24636  nrginvrcn  24641  nghmcn  24694  nmcn  24794  nmhmcn  25081  ipcnlem2  25205  ipcnlem1  25206  ipcn  25207  nglmle  25263  cssbn  25336  minveclem2  25387  minveclem3b  25389  minveclem3  25390  minveclem4  25393  minveclem7  25396