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

Theorem ngpgrp 20190
Description: A normed group is a group. (Contributed by Mario Carneiro, 2-Oct-2015.)
Assertion
Ref Expression
ngpgrp  |-  ( G  e. NrmGrp  ->  G  e.  Grp )

Proof of Theorem ngpgrp
StepHypRef Expression
1 eqid 2442 . . 3  |-  ( norm `  G )  =  (
norm `  G )
2 eqid 2442 . . 3  |-  ( -g `  G )  =  (
-g `  G )
3 eqid 2442 . . 3  |-  ( dist `  G )  =  (
dist `  G )
41, 2, 3isngp 20187 . 2  |-  ( G  e. NrmGrp 
<->  ( G  e.  Grp  /\  G  e.  MetSp  /\  (
( norm `  G )  o.  ( -g `  G
) )  C_  ( dist `  G ) ) )
54simp1bi 1003 1  |-  ( G  e. NrmGrp  ->  G  e.  Grp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756    C_ wss 3327    o. ccom 4843   ` cfv 5417   distcds 14246   Grpcgrp 15409   -gcsg 15412   MetSpcmt 19892   normcnm 20168  NrmGrpcngp 20169
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 2423
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 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-rex 2720  df-rab 2723  df-v 2973  df-dif 3330  df-un 3332  df-in 3334  df-ss 3341  df-nul 3637  df-if 3791  df-sn 3877  df-pr 3879  df-op 3883  df-uni 4091  df-br 4292  df-opab 4350  df-co 4848  df-iota 5380  df-fv 5425  df-ngp 20175
This theorem is referenced by:  ngpds  20194  ngpds2  20196  ngpds3  20198  ngprcan  20200  isngp4  20202  ngpinvds  20203  ngpsubcan  20204  nmf  20205  nmge0  20207  nmeq0  20208  nminv  20211  nmmtri  20212  nmsub  20213  nmrtri  20214  nm2dif  20215  nmtri  20216  nm0  20217  ngptgp  20221  tngngp2  20237  nlmdsdi  20261  nlmdsdir  20262  nrginvrcnlem  20270  nmo0  20313  nmotri  20317  0nghm  20319  nmoid  20320  idnghm  20321  nmods  20322  nmcn  20420  nmoleub2lem2  20670  nmhmcn  20674  ipcnlem2  20755  qqhcn  26419
  Copyright terms: Public domain W3C validator