Theorem ngpgrp 24564

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3889   ∘ ccom 5635  ‘cfv 6498  distcds 17229  Grpcgrp 18909  -_gcsg 18911  MetSpcms 24283  normcnm 24541  NrmGrpcngp 24542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-co 5640  df-iota 6454  df-fv 6506  df-ngp 24548

This theorem is referenced by:  ngpds  24569  ngpds2  24571  ngpds3  24573  ngprcan  24575  isngp4  24577  ngpinvds  24578  ngpsubcan  24579  nmf  24580  nmge0  24582  nmeq0  24583  nminv  24586  nmmtri  24587  nmsub  24588  nmrtri  24589  nm2dif  24590  nmtri  24591  nmtri2  24592  ngpi  24593  nm0  24594  ngptgp  24601  tngngp2  24617  tnggrpr  24620  nrmtngnrm  24623  nlmdsdi  24646  nlmdsdir  24647  nrginvrcnlem  24656  ngpocelbl  24669  nmo0  24700  nmotri  24704  0nghm  24706  nmoid  24707  idnghm  24708  nmods  24709  nmcn  24810  nmoleub2lem2  25083  nmhmcn  25087  cphpyth  25183  cphipval2  25208  4cphipval2  25209  cphipval  25210  ipcnlem2  25211  nglmle  25269  qqhcn  34135