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