Definition df-nrg 23195

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 23189	. 2 class NrmRing
2		vw	. . . . . 6 setvar 𝑤
3	2	cv 1536	. . . . 5 class 𝑤
4		cnm 23186	. . . . 5 class norm
5	3, 4	cfv 6355	. . . 4 class (norm‘𝑤)
6		cabv 19587	. . . . 5 class AbsVal
7	3, 6	cfv 6355	. . . 4 class (AbsVal‘𝑤)
8	5, 7	wcel 2114	. . 3 wff (norm‘𝑤) ∈ (AbsVal‘𝑤)
9		cngp 23187	. . 3 class NrmGrp
10	8, 2, 9	crab 3142	. 2 class {𝑤 ∈ NrmGrp ∣ (norm‘𝑤) ∈ (AbsVal‘𝑤)}
11	1, 10	wceq 1537	1 wff NrmRing = {𝑤 ∈ NrmGrp ∣ (norm‘𝑤) ∈ (AbsVal‘𝑤)}

This definition is referenced by:  isnrg  23269