Theorem ngpgrp 24927

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ⊆ wss 3896   ∘ ccom 5655  ‘cfv 6543  distcds 17446  Grpcgrp 19153  -_gcsg 19155  MetSpcms 24646  normcnm 24904  NrmGrpcngp 24905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-co 5660  df-iota 6497  df-fv 6551  df-ngp 24911

This theorem is used by:  ngpds  24932  ngpds2  24934  ngpds3  24936  ngprcan  24938  isngp4  24940  ngpinvds  24941  ngpsubcan  24942  nmf  24943  nmge0  24945  nmeq0  24946  nminv  24949  nmmtri  24950  nmsub  24951  nmrtri  24952  nm2dif  24953  nmtri  24954  nmtri2  24955  ngpi  24956  nm0  24957  ngptgp  24964  tngngp2  24980  tnggrpr  24983  nrmtngnrm  24986  nlmdsdi  25009  nlmdsdir  25010  nrginvrcnlem  25019  ngpocelbl  25032  nmo0  25063  nmotri  25067  0nghm  25069  nmoid  25070  idnghm  25071  nmods  25072  nmcn  25173  nmoleub2lem2  25446  nmhmcn  25450  cphpyth  25546  cphipval2  25571  4cphipval2  25572  cphipval  25573  ipcnlem2  25574  nglmle  25632  qqhcn  34673