Theorem ngpgrp 24627

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 24624	. 2 ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ((norm‘𝐺) ∘ (-g‘𝐺)) ⊆ (dist‘𝐺)))
5	4	simp1bi 1144	1 ⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ Grp)

Syntax hints:   → wi 4   ∈ wcel 2105   ⊆ wss 3962   ∘ ccom 5692  ‘cfv 6562  distcds 17306  Grpcgrp 18963  -_gcsg 18965  MetSpcms 24343  normcnm 24604  NrmGrpcngp 24605

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-co 5697  df-iota 6515  df-fv 6570  df-ngp 24611

This theorem is referenced by:  ngpds  24632  ngpds2  24634  ngpds3  24636  ngprcan  24638  isngp4  24640  ngpinvds  24641  ngpsubcan  24642  nmf  24643  nmge0  24645  nmeq0  24646  nminv  24649  nmmtri  24650  nmsub  24651  nmrtri  24652  nm2dif  24653  nmtri  24654  nmtri2  24655  ngpi  24656  nm0  24657  ngptgp  24664  tngngp2  24688  tnggrpr  24691  nrmtngnrm  24694  nlmdsdi  24717  nlmdsdir  24718  nrginvrcnlem  24727  ngpocelbl  24740  nmo0  24771  nmotri  24775  0nghm  24777  nmoid  24778  idnghm  24779  nmods  24780  nmcn  24879  nmoleub2lem2  25162  nmhmcn  25166  cphpyth  25263  cphipval2  25288  4cphipval2  25289  cphipval  25290  ipcnlem2  25291  nglmle  25349  qqhcn  33953