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

Theorem nrgngp 23871
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 2736 . . 3 (normβ€˜π‘…) = (normβ€˜π‘…)
2 eqid 2736 . . 3 (AbsValβ€˜π‘…) = (AbsValβ€˜π‘…)
31, 2isnrg 23869 . 2 (𝑅 ∈ NrmRing ↔ (𝑅 ∈ NrmGrp ∧ (normβ€˜π‘…) ∈ (AbsValβ€˜π‘…)))
43simplbi 499 1 (𝑅 ∈ NrmRing β†’ 𝑅 ∈ NrmGrp)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∈ wcel 2104  β€˜cfv 6458  AbsValcabv 20121  normcnm 23777  NrmGrpcngp 23778  NrmRingcnrg 23780
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-iota 6410  df-fv 6466  df-nrg 23786
This theorem is referenced by:  nrgdsdi  23874  nrgdsdir  23875  unitnmn0  23877  nminvr  23878  nmdvr  23879  nrgtgp  23881  subrgnrg  23882  nlmngp2  23889  sranlm  23893  nrginvrcnlem  23900  nrginvrcn  23901  cnzh  31965  rezh  31966  qqhcn  31986  qqhucn  31987  rrhcn  31992  rrhf  31993  rrexttps  32001  rrexthaus  32002
  Copyright terms: Public domain W3C validator