Definition df-nrg 22390

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.)

Assertion

Ref	Expression
df-nrg	|- NrmRing = { w e. NrmGrp | ( norm ` w ) e. (AbsVal ` w ) }

Detailed syntax breakdown of Definition df-nrg

Step	Hyp	Ref	Expression
1		cnrg 22384	. 2 class NrmRing
2		vw	. . . . . 6 setvar w
3	2	cv 1482	. . . . 5 class w
4		cnm 22381	. . . . 5 class norm
5	3, 4	cfv 5888	. . . 4 class ( norm ` w )
6		cabv 18816	. . . . 5 class AbsVal
7	3, 6	cfv 5888	. . . 4 class (AbsVal ` w )
8	5, 7	wcel 1990	. . 3 wff ( norm ` w ) e. (AbsVal ` w )
9		cngp 22382	. . 3 class NrmGrp
10	8, 2, 9	crab 2916	. 2 class { w e. NrmGrp | ( norm ` w ) e. (AbsVal ` w ) }
11	1, 10	wceq 1483	1 wff NrmRing = { w e. NrmGrp | ( norm ` w ) e. (AbsVal ` w ) }

This definition is referenced by:  isnrg  22464