Theorem ngpgrp 24541

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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3899   ∘ ccom 5626  ‘cfv 6490  distcds 17184  Grpcgrp 18861  -_gcsg 18863  MetSpcms 24260  normcnm 24518  NrmGrpcngp 24519

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-co 5631  df-iota 6446  df-fv 6498  df-ngp 24525

This theorem is referenced by:  ngpds  24546  ngpds2  24548  ngpds3  24550  ngprcan  24552  isngp4  24554  ngpinvds  24555  ngpsubcan  24556  nmf  24557  nmge0  24559  nmeq0  24560  nminv  24563  nmmtri  24564  nmsub  24565  nmrtri  24566  nm2dif  24567  nmtri  24568  nmtri2  24569  ngpi  24570  nm0  24571  ngptgp  24578  tngngp2  24594  tnggrpr  24597  nrmtngnrm  24600  nlmdsdi  24623  nlmdsdir  24624  nrginvrcnlem  24633  ngpocelbl  24646  nmo0  24677  nmotri  24681  0nghm  24683  nmoid  24684  idnghm  24685  nmods  24686  nmcn  24787  nmoleub2lem2  25070  nmhmcn  25074  cphpyth  25170  cphipval2  25195  4cphipval2  25196  cphipval  25197  ipcnlem2  25198  nglmle  25256  qqhcn  34097