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

Theorem ngpms 20848
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 2460 . . 3  |-  ( norm `  G )  =  (
norm `  G )
2 eqid 2460 . . 3  |-  ( -g `  G )  =  (
-g `  G )
3 eqid 2460 . . 3  |-  ( dist `  G )  =  (
dist `  G )
41, 2, 3isngp 20844 . 2  |-  ( G  e. NrmGrp 
<->  ( G  e.  Grp  /\  G  e.  MetSp  /\  (
( norm `  G )  o.  ( -g `  G
) )  C_  ( dist `  G ) ) )
54simp2bi 1007 1  |-  ( G  e. NrmGrp  ->  G  e.  MetSp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1762    C_ wss 3469    o. ccom 4996   ` cfv 5579   distcds 14553   Grpcgrp 15716   -gcsg 15719   MetSpcmt 20549   normcnm 20825  NrmGrpcngp 20826
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-co 5001  df-iota 5542  df-fv 5587  df-ngp 20832
This theorem is referenced by:  ngpxms  20849  ngptps  20850  isngp4  20859  nmf  20862  nmmtri  20869  nmrtri  20871  subgngp  20877  ngptgp  20878  tngngp2  20894  nlmvscnlem2  20922  nlmvscnlem1  20923  nlmvscn  20924  nrginvrcn  20928  nghmcn  20980  nmcn  21077  nmhmcn  21331  ipcnlem2  21412  ipcnlem1  21413  ipcn  21414  minveclem2  21569  minveclem3b  21571  minveclem3  21572  minveclem4  21575  minveclem7  21578
  Copyright terms: Public domain W3C validator