Theorem ngpms 24523

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3911   ∘ ccom 5635  ‘cfv 6500  distcds 17207  Grpcgrp 18849  -_gcsg 18851  MetSpcms 24241  normcnm 24499  NrmGrpcngp 24500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-co 5640  df-iota 6453  df-fv 6508  df-ngp 24506

This theorem is referenced by:  ngpxms  24524  ngptps  24525  ngpmet  24526  isngp4  24535  nmmtri  24545  nmrtri  24547  subgngp  24558  ngptgp  24559  tngngp2  24575  nlmvscnlem2  24608  nlmvscnlem1  24609  nlmvscn  24610  nrginvrcn  24615  nghmcn  24668  nmcn  24768  nmhmcn  25055  ipcnlem2  25179  ipcnlem1  25180  ipcn  25181  nglmle  25237  cssbn  25310  minveclem2  25361  minveclem3b  25363  minveclem3  25364  minveclem4  25367  minveclem7  25370