Theorem ngpms 24109

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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3949   ∘ ccom 5681  ‘cfv 6544  distcds 17206  Grpcgrp 18819  -_gcsg 18821  MetSpcms 23824  normcnm 24085  NrmGrpcngp 24086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-co 5686  df-iota 6496  df-fv 6552  df-ngp 24092

This theorem is referenced by:  ngpxms  24110  ngptps  24111  ngpmet  24112  isngp4  24121  nmmtri  24131  nmrtri  24133  subgngp  24144  ngptgp  24145  tngngp2  24169  nlmvscnlem2  24202  nlmvscnlem1  24203  nlmvscn  24204  nrginvrcn  24209  nghmcn  24262  nmcn  24360  nmhmcn  24636  ipcnlem2  24761  ipcnlem1  24762  ipcn  24763  nglmle  24819  cssbn  24892  minveclem2  24943  minveclem3b  24945  minveclem3  24946  minveclem4  24949  minveclem7  24952