Theorem ngpgrp 24577

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 2737	. . 3 ⊢ (norm‘𝐺) = (norm‘𝐺)
2		eqid 2737	. . 3 ⊢ (-g‘𝐺) = (-g‘𝐺)
3		eqid 2737	. . 3 ⊢ (dist‘𝐺) = (dist‘𝐺)
4	1, 2, 3	isngp 24574	. 2 ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ((norm‘𝐺) ∘ (-g‘𝐺)) ⊆ (dist‘𝐺)))
5	4	simp1bi 1146	1 ⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ Grp)

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890   ∘ ccom 5629  ‘cfv 6493  distcds 17223  Grpcgrp 18903  -_gcsg 18905  MetSpcms 24296  normcnm 24554  NrmGrpcngp 24555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-co 5634  df-iota 6449  df-fv 6501  df-ngp 24561

This theorem is referenced by:  ngpds  24582  ngpds2  24584  ngpds3  24586  ngprcan  24588  isngp4  24590  ngpinvds  24591  ngpsubcan  24592  nmf  24593  nmge0  24595  nmeq0  24596  nminv  24599  nmmtri  24600  nmsub  24601  nmrtri  24602  nm2dif  24603  nmtri  24604  nmtri2  24605  ngpi  24606  nm0  24607  ngptgp  24614  tngngp2  24630  tnggrpr  24633  nrmtngnrm  24636  nlmdsdi  24659  nlmdsdir  24660  nrginvrcnlem  24669  ngpocelbl  24682  nmo0  24713  nmotri  24717  0nghm  24719  nmoid  24720  idnghm  24721  nmods  24722  nmcn  24823  nmoleub2lem2  25096  nmhmcn  25100  cphpyth  25196  cphipval2  25221  4cphipval2  25222  cphipval  25223  ipcnlem2  25224  nglmle  25282  qqhcn  34154