Theorem ngpgrp 24536

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3926   ∘ ccom 5658  ‘cfv 6530  distcds 17278  Grpcgrp 18914  -_gcsg 18916  MetSpcms 24255  normcnm 24513  NrmGrpcngp 24514

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-co 5663  df-iota 6483  df-fv 6538  df-ngp 24520

This theorem is referenced by:  ngpds  24541  ngpds2  24543  ngpds3  24545  ngprcan  24547  isngp4  24549  ngpinvds  24550  ngpsubcan  24551  nmf  24552  nmge0  24554  nmeq0  24555  nminv  24558  nmmtri  24559  nmsub  24560  nmrtri  24561  nm2dif  24562  nmtri  24563  nmtri2  24564  ngpi  24565  nm0  24566  ngptgp  24573  tngngp2  24589  tnggrpr  24592  nrmtngnrm  24595  nlmdsdi  24618  nlmdsdir  24619  nrginvrcnlem  24628  ngpocelbl  24641  nmo0  24672  nmotri  24676  0nghm  24678  nmoid  24679  idnghm  24680  nmods  24681  nmcn  24782  nmoleub2lem2  25065  nmhmcn  25069  cphpyth  25166  cphipval2  25191  4cphipval2  25192  cphipval  25193  ipcnlem2  25194  nglmle  25252  qqhcn  33968