Theorem ngpms 23209

Description: A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)

Assertion

Ref	Expression
ngpms	⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp)

Proof of Theorem ngpms

Step	Hyp	Ref	Expression
1		eqid 2821	. . 3 ⊢ (norm‘𝐺) = (norm‘𝐺)
2		eqid 2821	. . 3 ⊢ (-g‘𝐺) = (-g‘𝐺)
3		eqid 2821	. . 3 ⊢ (dist‘𝐺) = (dist‘𝐺)
4	1, 2, 3	isngp 23205	. 2 ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ((norm‘𝐺) ∘ (-g‘𝐺)) ⊆ (dist‘𝐺)))
5	4	simp2bi 1142	1 ⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp)

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3936   ∘ ccom 5559  ‘cfv 6355  distcds 16574  Grpcgrp 18103  -_gcsg 18105  MetSpcms 22928  normcnm 23186  NrmGrpcngp 23187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-co 5564  df-iota 6314  df-fv 6363  df-ngp 23193

This theorem is referenced by:  ngpxms  23210  ngptps  23211  ngpmet  23212  isngp4  23221  nmmtri  23231  nmrtri  23233  subgngp  23244  ngptgp  23245  tngngp2  23261  nlmvscnlem2  23294  nlmvscnlem1  23295  nlmvscn  23296  nrginvrcn  23301  nghmcn  23354  nmcn  23452  nmhmcn  23724  ipcnlem2  23847  ipcnlem1  23848  ipcn  23849  nglmle  23905  cssbn  23978  minveclem2  24029  minveclem3b  24031  minveclem3  24032  minveclem4  24035  minveclem7  24038