# Metamath Proof Explorer

## Theorem isnrg

Description: A normed ring is a ring with a norm that makes it into a normed group, and such that the norm is an absolute value on the ring. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses isnrg.1 ${⊢}{N}=\mathrm{norm}\left({R}\right)$
isnrg.2 ${⊢}{A}=\mathrm{AbsVal}\left({R}\right)$
Assertion isnrg ${⊢}{R}\in \mathrm{NrmRing}↔\left({R}\in \mathrm{NrmGrp}\wedge {N}\in {A}\right)$

### Proof

Step Hyp Ref Expression
1 isnrg.1 ${⊢}{N}=\mathrm{norm}\left({R}\right)$
2 isnrg.2 ${⊢}{A}=\mathrm{AbsVal}\left({R}\right)$
3 fveq2 ${⊢}{r}={R}\to \mathrm{norm}\left({r}\right)=\mathrm{norm}\left({R}\right)$
4 3 1 eqtr4di ${⊢}{r}={R}\to \mathrm{norm}\left({r}\right)={N}$
5 fveq2 ${⊢}{r}={R}\to \mathrm{AbsVal}\left({r}\right)=\mathrm{AbsVal}\left({R}\right)$
6 5 2 eqtr4di ${⊢}{r}={R}\to \mathrm{AbsVal}\left({r}\right)={A}$
7 4 6 eleq12d ${⊢}{r}={R}\to \left(\mathrm{norm}\left({r}\right)\in \mathrm{AbsVal}\left({r}\right)↔{N}\in {A}\right)$
8 df-nrg ${⊢}\mathrm{NrmRing}=\left\{{r}\in \mathrm{NrmGrp}|\mathrm{norm}\left({r}\right)\in \mathrm{AbsVal}\left({r}\right)\right\}$
9 7 8 elrab2 ${⊢}{R}\in \mathrm{NrmRing}↔\left({R}\in \mathrm{NrmGrp}\wedge {N}\in {A}\right)$