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

Theorem ngpgrp 18223
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 2358 . . 3  |-  ( norm `  G )  =  (
norm `  G )
2 eqid 2358 . . 3  |-  ( -g `  G )  =  (
-g `  G )
3 eqid 2358 . . 3  |-  ( dist `  G )  =  (
dist `  G )
41, 2, 3isngp 18220 . 2  |-  ( G  e. NrmGrp 
<->  ( G  e.  Grp  /\  G  e.  MetSp  /\  (
( norm `  G )  o.  ( -g `  G
) )  C_  ( dist `  G ) ) )
54simp1bi 970 1  |-  ( G  e. NrmGrp  ->  G  e.  Grp )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1710    C_ wss 3228    o. ccom 4775   ` cfv 5337   distcds 13314   Grpcgrp 14461   -gcsg 14464   MetSpcmt 17985   normcnm 18201  NrmGrpcngp 18202
This theorem is referenced by:  ngpds  18227  ngpds2  18229  ngpds3  18231  ngprcan  18233  isngp4  18235  ngpinvds  18236  ngpsubcan  18237  nmf  18238  nmge0  18240  nmeq0  18241  nminv  18244  nmmtri  18245  nmsub  18246  nmrtri  18247  nm2dif  18248  nmtri  18249  nm0  18250  ngptgp  18254  tngngp2  18270  nlmdsdi  18294  nlmdsdir  18295  nrginvrcnlem  18303  nmo0  18346  nmotri  18350  0nghm  18352  nmoid  18353  idnghm  18354  nmods  18355  nmcn  18452  nmoleub2lem2  18701  nmhmcn  18705  ipcnlem2  18775  qqhcn  23648
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rex 2625  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-br 4105  df-opab 4159  df-co 4780  df-iota 5301  df-fv 5345  df-ngp 18208
  Copyright terms: Public domain W3C validator