Theorem ngpms 23201

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3934   ∘ ccom 5552  ‘cfv 6348  distcds 16566  Grpcgrp 18095  -_gcsg 18097  MetSpcms 22920  normcnm 23178  NrmGrpcngp 23179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-co 5557  df-iota 6307  df-fv 6356  df-ngp 23185

This theorem is referenced by:  ngpxms  23202  ngptps  23203  ngpmet  23204  isngp4  23213  nmmtri  23223  nmrtri  23225  subgngp  23236  ngptgp  23237  tngngp2  23253  nlmvscnlem2  23286  nlmvscnlem1  23287  nlmvscn  23288  nrginvrcn  23293  nghmcn  23346  nmcn  23444  nmhmcn  23716  ipcnlem2  23839  ipcnlem1  23840  ipcn  23841  nglmle  23897  cssbn  23970  minveclem2  24021  minveclem3b  24023  minveclem3  24024  minveclem4  24027  minveclem7  24030