Theorem ngpgrp 23201

Description: A normed group is a group. (Contributed by Mario Carneiro, 2-Oct-2015.)

Assertion

Ref	Expression
ngpgrp	⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ Grp)

Proof of Theorem ngpgrp

Step	Hyp	Ref	Expression
1		eqid 2820	. . 3 ⊢ (norm‘𝐺) = (norm‘𝐺)
2		eqid 2820	. . 3 ⊢ (-g‘𝐺) = (-g‘𝐺)
3		eqid 2820	. . 3 ⊢ (dist‘𝐺) = (dist‘𝐺)
4	1, 2, 3	isngp 23198	. 2 ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ((norm‘𝐺) ∘ (-g‘𝐺)) ⊆ (dist‘𝐺)))
5	4	simp1bi 1140	1 ⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ Grp)

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3929   ∘ ccom 5552  ‘cfv 6348  distcds 16567  Grpcgrp 18096  -_gcsg 18098  MetSpcms 22921  normcnm 23179  NrmGrpcngp 23180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-rab 3146  df-v 3493  df-dif 3932  df-un 3934  df-in 3936  df-ss 3945  df-nul 4285  df-if 4461  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5060  df-opab 5122  df-co 5557  df-iota 6307  df-fv 6356  df-ngp 23186

This theorem is referenced by:  ngpds  23206  ngpds2  23208  ngpds3  23210  ngprcan  23212  isngp4  23214  ngpinvds  23215  ngpsubcan  23216  nmf  23217  nmge0  23219  nmeq0  23220  nminv  23223  nmmtri  23224  nmsub  23225  nmrtri  23226  nm2dif  23227  nmtri  23228  nmtri2  23229  ngpi  23230  nm0  23231  ngptgp  23238  tngngp2  23254  tnggrpr  23257  nrmtngnrm  23260  nlmdsdi  23283  nlmdsdir  23284  nrginvrcnlem  23293  ngpocelbl  23306  nmo0  23337  nmotri  23341  0nghm  23343  nmoid  23344  idnghm  23345  nmods  23346  nmcn  23445  nmoleub2lem2  23713  nmhmcn  23717  cphipval2  23837  4cphipval2  23838  cphipval  23839  ipcnlem2  23840  nglmle  23898  qqhcn  31251