Theorem ngpgrp 22815

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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3792   ∘ ccom 5361  ‘cfv 6137  distcds 16351  Grpcgrp 17813  -_gcsg 17815  MetSpcms 22535  normcnm 22793  NrmGrpcngp 22794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-co 5366  df-iota 6101  df-fv 6145  df-ngp 22800

This theorem is referenced by:  ngpds  22820  ngpds2  22822  ngpds3  22824  ngprcan  22826  isngp4  22828  ngpinvds  22829  ngpsubcan  22830  nmf  22831  nmge0  22833  nmeq0  22834  nminv  22837  nmmtri  22838  nmsub  22839  nmrtri  22840  nm2dif  22841  nmtri  22842  nmtri2  22843  ngpi  22844  nm0  22845  ngptgp  22852  tngngp2  22868  tnggrpr  22871  nrmtngnrm  22874  nlmdsdi  22897  nlmdsdir  22898  nrginvrcnlem  22907  ngpocelbl  22920  nmo0  22951  nmotri  22955  0nghm  22957  nmoid  22958  idnghm  22959  nmods  22960  nmcn  23059  nmoleub2lem2  23327  nmhmcn  23331  cphipval2  23451  4cphipval2  23452  cphipval  23453  ipcnlem2  23454  nglmle  23512  qqhcn  30637