Theorem ngpgrp 24463

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3911   ∘ ccom 5635  ‘cfv 6499  distcds 17205  Grpcgrp 18841  -_gcsg 18843  MetSpcms 24182  normcnm 24440  NrmGrpcngp 24441

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-co 5640  df-iota 6452  df-fv 6507  df-ngp 24447

This theorem is referenced by:  ngpds  24468  ngpds2  24470  ngpds3  24472  ngprcan  24474  isngp4  24476  ngpinvds  24477  ngpsubcan  24478  nmf  24479  nmge0  24481  nmeq0  24482  nminv  24485  nmmtri  24486  nmsub  24487  nmrtri  24488  nm2dif  24489  nmtri  24490  nmtri2  24491  ngpi  24492  nm0  24493  ngptgp  24500  tngngp2  24516  tnggrpr  24519  nrmtngnrm  24522  nlmdsdi  24545  nlmdsdir  24546  nrginvrcnlem  24555  ngpocelbl  24568  nmo0  24599  nmotri  24603  0nghm  24605  nmoid  24606  idnghm  24607  nmods  24608  nmcn  24709  nmoleub2lem2  24992  nmhmcn  24996  cphpyth  25092  cphipval2  25117  4cphipval2  25118  cphipval  25119  ipcnlem2  25120  nglmle  25178  qqhcn  33954