Definition df-nrg

Description: A normed ring is a ring with an induced topology and metric such that the metric is translation-invariant and the norm (distance from 0) is an absolute value on the ring. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Assertion	df-nrg	$$⊢\mathrm{NrmRing}=\left\{w\in \mathrm{NrmGrp}|\mathrm{norm}\left(w\right)\in \mathrm{AbsVal}\left(w\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnrg	$$class\mathrm{NrmRing}$$
1		vw	$$setvarw$$
2		cngp	$$class\mathrm{NrmGrp}$$
3		cnm	$$class\mathrm{norm}$$
4	1	cv	$$setvarw$$
5	4 3	cfv	$$class\mathrm{norm}\left(w\right)$$
6		cabv	$$class\mathrm{AbsVal}$$
7	4 6	cfv	$$class\mathrm{AbsVal}\left(w\right)$$
8	5 7	wcel	$$wff\mathrm{norm}\left(w\right)\in \mathrm{AbsVal}\left(w\right)$$
9	8 1 2	crab	$$class\left\{w\in \mathrm{NrmGrp}|\mathrm{norm}\left(w\right)\in \mathrm{AbsVal}\left(w\right)\right\}$$
10	0 9	wceq	$$wff\mathrm{NrmRing}=\left\{w\in \mathrm{NrmGrp}|\mathrm{norm}\left(w\right)\in \mathrm{AbsVal}\left(w\right)\right\}$$