Theorem ngpgrp 22403

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

Syntax hints:   → wi 4   ∈ wcel 1990   ⊆ wss 3574   ∘ ccom 5118  ‘cfv 5888  distcds 15950  Grpcgrp 17422  -_gcsg 17424  MetSpcmt 22123  normcnm 22381  NrmGrpcngp 22382

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-co 5123  df-iota 5851  df-fv 5896  df-ngp 22388

This theorem is referenced by:  ngpds  22408  ngpds2  22410  ngpds3  22412  ngprcan  22414  isngp4  22416  ngpinvds  22417  ngpsubcan  22418  nmf  22419  nmge0  22421  nmeq0  22422  nminv  22425  nmmtri  22426  nmsub  22427  nmrtri  22428  nm2dif  22429  nmtri  22430  nmtri2  22431  ngpi  22432  nm0  22433  ngptgp  22440  tngngp2  22456  tnggrpr  22459  nrmtngnrm  22462  nlmdsdi  22485  nlmdsdir  22486  nrginvrcnlem  22495  ngpocelbl  22508  nmo0  22539  nmotri  22543  0nghm  22545  nmoid  22546  idnghm  22547  nmods  22548  nmcn  22647  nmoleub2lem2  22916  nmhmcn  22920  cphipval2  23040  4cphipval2  23041  cphipval  23042  ipcnlem2  23043  nglmle  23100  qqhcn  30035