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	|- NrmRing = { w e. NrmGrp | ( norm ` w ) e. ( AbsVal ` w ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnrg	|- NrmRing
1		vw	|- w
2		cngp	|- NrmGrp
3		cnm	|- norm
4	1	cv	|- w
5	4 3	cfv	|- ( norm ` w )
6		cabv	|- AbsVal
7	4 6	cfv	|- ( AbsVal ` w )
8	5 7	wcel	|- ( norm ` w ) e. ( AbsVal ` w )
9	8 1 2	crab	|- { w e. NrmGrp | ( norm ` w ) e. ( AbsVal ` w ) }
10	0 9	wceq	|- NrmRing = { w e. NrmGrp | ( norm ` w ) e. ( AbsVal ` w ) }