Definition df-nrg 24598

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 24592	. 2 class NrmRing
2		vw	. . . . . 6 setvar 𝑤
3	2	cv 1539	. . . . 5 class 𝑤
4		cnm 24589	. . . . 5 class norm
5	3, 4	cfv 6561	. . . 4 class (norm‘𝑤)
6		cabv 20809	. . . . 5 class AbsVal
7	3, 6	cfv 6561	. . . 4 class (AbsVal‘𝑤)
8	5, 7	wcel 2108	. . 3 wff (norm‘𝑤) ∈ (AbsVal‘𝑤)
9		cngp 24590	. . 3 class NrmGrp
10	8, 2, 9	crab 3436	. 2 class {𝑤 ∈ NrmGrp ∣ (norm‘𝑤) ∈ (AbsVal‘𝑤)}
11	1, 10	wceq 1540	1 wff NrmRing = {𝑤 ∈ NrmGrp ∣ (norm‘𝑤) ∈ (AbsVal‘𝑤)}

This definition is referenced by:  isnrg  24681