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

Theorem ngpms 20034
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 2433 . . 3  |-  ( norm `  G )  =  (
norm `  G )
2 eqid 2433 . . 3  |-  ( -g `  G )  =  (
-g `  G )
3 eqid 2433 . . 3  |-  ( dist `  G )  =  (
dist `  G )
41, 2, 3isngp 20030 . 2  |-  ( G  e. NrmGrp 
<->  ( G  e.  Grp  /\  G  e.  MetSp  /\  (
( norm `  G )  o.  ( -g `  G
) )  C_  ( dist `  G ) ) )
54simp2bi 997 1  |-  ( G  e. NrmGrp  ->  G  e.  MetSp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755    C_ wss 3316    o. ccom 4831   ` cfv 5406   distcds 14230   Grpcgrp 15393   -gcsg 15396   MetSpcmt 19735   normcnm 20011  NrmGrpcngp 20012
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-co 4836  df-iota 5369  df-fv 5414  df-ngp 20018
This theorem is referenced by:  ngpxms  20035  ngptps  20036  isngp4  20045  nmf  20048  nmmtri  20055  nmrtri  20057  subgngp  20063  ngptgp  20064  tngngp2  20080  nlmvscnlem2  20108  nlmvscnlem1  20109  nlmvscn  20110  nrginvrcn  20114  nghmcn  20166  nmcn  20263  nmhmcn  20517  ipcnlem2  20598  ipcnlem1  20599  ipcn  20600  minveclem2  20755  minveclem3b  20757  minveclem3  20758  minveclem4  20761  minveclem7  20764
  Copyright terms: Public domain W3C validator