Definition df-nrg 23722

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 = {𝑤 ∈ NrmGrp ∣ (norm‘𝑤) ∈ (AbsVal‘𝑤)}

Detailed syntax breakdown of Definition df-nrg

Step	Hyp	Ref	Expression
1		cnrg 23716	. 2 class NrmRing
2		vw	. . . . . 6 setvar 𝑤
3	2	cv 1540	. . . . 5 class 𝑤
4		cnm 23713	. . . . 5 class norm
5	3, 4	cfv 6430	. . . 4 class (norm‘𝑤)
6		cabv 20057	. . . . 5 class AbsVal
7	3, 6	cfv 6430	. . . 4 class (AbsVal‘𝑤)
8	5, 7	wcel 2109	. . 3 wff (norm‘𝑤) ∈ (AbsVal‘𝑤)
9		cngp 23714	. . 3 class NrmGrp
10	8, 2, 9	crab 3069	. 2 class {𝑤 ∈ NrmGrp ∣ (norm‘𝑤) ∈ (AbsVal‘𝑤)}
11	1, 10	wceq 1541	1 wff NrmRing = {𝑤 ∈ NrmGrp ∣ (norm‘𝑤) ∈ (AbsVal‘𝑤)}

This definition is referenced by:  isnrg  23805