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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnrg	⊢ NrmRing
1		vw	⊢ 𝑤
2		cngp	⊢ NrmGrp
3		cnm	⊢ norm
4	1	cv	⊢ 𝑤
5	4 3	cfv	⊢ ( norm ‘ 𝑤 )
6		cabv	⊢ AbsVal
7	4 6	cfv	⊢ ( AbsVal ‘ 𝑤 )
8	5 7	wcel	⊢ ( norm ‘ 𝑤 ) ∈ ( AbsVal ‘ 𝑤 )
9	8 1 2	crab	⊢ { 𝑤 ∈ NrmGrp ∣ ( norm ‘ 𝑤 ) ∈ ( AbsVal ‘ 𝑤 ) }
10	0 9	wceq	⊢ NrmRing = { 𝑤 ∈ NrmGrp ∣ ( norm ‘ 𝑤 ) ∈ ( AbsVal ‘ 𝑤 ) }