Theorem nrgngp 24889

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 2762	. . 3 ⊢ (norm‘𝑅) = (norm‘𝑅)
2		eqid 2762	. . 3 ⊢ (AbsVal‘𝑅) = (AbsVal‘𝑅)
3	1, 2	isnrg 24887	. 2 ⊢ (𝑅 ∈ NrmRing ↔ (𝑅 ∈ NrmGrp ∧ (norm‘𝑅) ∈ (AbsVal‘𝑅)))
4	3	simplbi 502	1 ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6537  AbsValcabv 20975  normcnm 24803  NrmGrpcngp 24804  NrmRingcnrg 24806

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-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-nrg 24812

This theorem is used by:  nrgdsdi  24892  nrgdsdir  24893  unitnmn0  24895  nminvr  24896  nmdvr  24897  nrgtgp  24899  subrgnrg  24900  nlmngp2  24907  sranlm  24911  nrginvrcnlem  24918  nrginvrcn  24919  cnzh  34465  rezh  34466  qqhcn  34488  qqhucn  34489  rrhcn  34494  rrhf  34495  rrexttps  34503  rrexthaus  34504