MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ngpms Structured version   Unicode version

Theorem ngpms 20172
Description: A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
Assertion
Ref Expression
ngpms  |-  ( G  e. NrmGrp  ->  G  e.  MetSp )

Proof of Theorem ngpms
StepHypRef Expression
1 eqid 2438 . . 3  |-  ( norm `  G )  =  (
norm `  G )
2 eqid 2438 . . 3  |-  ( -g `  G )  =  (
-g `  G )
3 eqid 2438 . . 3  |-  ( dist `  G )  =  (
dist `  G )
41, 2, 3isngp 20168 . 2  |-  ( G  e. NrmGrp 
<->  ( G  e.  Grp  /\  G  e.  MetSp  /\  (
( norm `  G )  o.  ( -g `  G
) )  C_  ( dist `  G ) ) )
54simp2bi 1004 1  |-  ( G  e. NrmGrp  ->  G  e.  MetSp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756    C_ wss 3323    o. ccom 4839   ` cfv 5413   distcds 14239   Grpcgrp 15402   -gcsg 15405   MetSpcmt 19873   normcnm 20149  NrmGrpcngp 20150
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-co 4844  df-iota 5376  df-fv 5421  df-ngp 20156
This theorem is referenced by:  ngpxms  20173  ngptps  20174  isngp4  20183  nmf  20186  nmmtri  20193  nmrtri  20195  subgngp  20201  ngptgp  20202  tngngp2  20218  nlmvscnlem2  20246  nlmvscnlem1  20247  nlmvscn  20248  nrginvrcn  20252  nghmcn  20304  nmcn  20401  nmhmcn  20655  ipcnlem2  20736  ipcnlem1  20737  ipcn  20738  minveclem2  20893  minveclem3b  20895  minveclem3  20896  minveclem4  20899  minveclem7  20902
  Copyright terms: Public domain W3C validator