Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nrgngp Structured version   Visualization version   GIF version

Theorem nrgngp 23247
 Description: A normed ring is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
Assertion
Ref Expression
nrgngp (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp)

Proof of Theorem nrgngp
StepHypRef Expression
1 eqid 2821 . . 3 (norm‘𝑅) = (norm‘𝑅)
2 eqid 2821 . . 3 (AbsVal‘𝑅) = (AbsVal‘𝑅)
31, 2isnrg 23245 . 2 (𝑅 ∈ NrmRing ↔ (𝑅 ∈ NrmGrp ∧ (norm‘𝑅) ∈ (AbsVal‘𝑅)))
43simplbi 501 1 (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2115  ‘cfv 6328  AbsValcabv 19563  normcnm 23162  NrmGrpcngp 23163  NrmRingcnrg 23165 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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-rab 3135  df-v 3473  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-br 5040  df-iota 6287  df-fv 6336  df-nrg 23171 This theorem is referenced by:  nrgdsdi  23250  nrgdsdir  23251  unitnmn0  23253  nminvr  23254  nmdvr  23255  nrgtgp  23257  subrgnrg  23258  nlmngp2  23265  sranlm  23269  nrginvrcnlem  23276  nrginvrcn  23277  cnzh  31219  rezh  31220  qqhcn  31240  qqhucn  31241  rrhcn  31246  rrhf  31247  rrexttps  31255  rrexthaus  31256
 Copyright terms: Public domain W3C validator