Theorem nrgngp 24620

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

Step	Hyp	Ref	Expression
1		eqid 2734	. . 3 ⊢ (norm‘𝑅) = (norm‘𝑅)
2		eqid 2734	. . 3 ⊢ (AbsVal‘𝑅) = (AbsVal‘𝑅)
3	1, 2	isnrg 24618	. 2 ⊢ (𝑅 ∈ NrmRing ↔ (𝑅 ∈ NrmGrp ∧ (norm‘𝑅) ∈ (AbsVal‘𝑅)))
4	3	simplbi 497	1 ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp)

Syntax hints:   → wi 4   ∈ wcel 2107  ‘cfv 6541  AbsValcabv 20778  normcnm 24534  NrmGrpcngp 24535  NrmRingcnrg 24537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-iota 6494  df-fv 6549  df-nrg 24543

This theorem is referenced by:  nrgdsdi  24623  nrgdsdir  24624  unitnmn0  24626  nminvr  24627  nmdvr  24628  nrgtgp  24630  subrgnrg  24631  nlmngp2  24638  sranlm  24642  nrginvrcnlem  24649  nrginvrcn  24650  cnzh  33944  rezh  33945  qqhcn  33967  qqhucn  33968  rrhcn  33973  rrhf  33974  rrexttps  33982  rrexthaus  33983