Metamath Proof Explorer

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 = w ∈ NrmGrp | norm ⁡ w ∈ AbsVal ⁡ w

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnrg class NrmRing
1 vw setvar w
2 cngp class NrmGrp
3 cnm class norm
4 1 cv setvar w
5 4 3 cfv class norm ⁡ w
6 cabv class AbsVal
7 4 6 cfv class AbsVal ⁡ w
8 5 7 wcel wff norm ⁡ w ∈ AbsVal ⁡ w
9 8 1 2 crab class w ∈ NrmGrp | norm ⁡ w ∈ AbsVal ⁡ w
10 0 9 wceq wff NrmRing = w ∈ NrmGrp | norm ⁡ w ∈ AbsVal ⁡ w