Theorem ngpms 24827

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3902   ∘ ccom 5663  ‘cfv 6537  distcds 17355  Grpcgrp 19058  -_gcsg 19060  MetSpcms 24545  normcnm 24803  NrmGrpcngp 24804

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-co 5668  df-iota 6493  df-fv 6545  df-ngp 24810

This theorem is used by:  ngpxms  24828  ngptps  24829  ngpmet  24830  isngp4  24839  nmmtri  24849  nmrtri  24851  subgngp  24862  ngptgp  24863  tngngp2  24879  nlmvscnlem2  24912  nlmvscnlem1  24913  nlmvscn  24914  nrginvrcn  24919  nghmcn  24972  nmcn  25072  nmhmcn  25349  ipcnlem2  25473  ipcnlem1  25474  ipcn  25475  nglmle  25531  cssbn  25604  minveclem2  25655  minveclem3b  25657  minveclem3  25658  minveclem4  25661  minveclem7  25664