This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nrgngp

Description: A normed ring is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Assertion nrgngp ⊢ R ∈ NrmRing → R ∈ NrmGrp

Proof

Step Hyp Ref Expression
1 eqid ⊢ norm ⁡ R = norm ⁡ R
2 eqid ⊢ AbsVal ⁡ R = AbsVal ⁡ R
3 1 2 isnrg ⊢ R ∈ NrmRing ↔ R ∈ NrmGrp ∧ norm ⁡ R ∈ AbsVal ⁡ R
4 3 simplbi ⊢ R ∈ NrmRing → R ∈ NrmGrp