MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nrg Structured version   Unicode version

Definition df-nrg 20979
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  =  {
w  e. NrmGrp  |  ( norm `  w )  e.  (AbsVal `  w ) }

Detailed syntax breakdown of Definition df-nrg
StepHypRef Expression
1 cnrg 20973 . 2  class NrmRing
2 vw . . . . . 6  setvar  w
32cv 1382 . . . . 5  class  w
4 cnm 20970 . . . . 5  class  norm
53, 4cfv 5578 . . . 4  class  ( norm `  w )
6 cabv 17339 . . . . 5  class AbsVal
73, 6cfv 5578 . . . 4  class  (AbsVal `  w )
85, 7wcel 1804 . . 3  wff  ( norm `  w )  e.  (AbsVal `  w )
9 cngp 20971 . . 3  class NrmGrp
108, 2, 9crab 2797 . 2  class  { w  e. NrmGrp  |  ( norm `  w
)  e.  (AbsVal `  w ) }
111, 10wceq 1383 1  wff NrmRing  =  {
w  e. NrmGrp  |  ( norm `  w )  e.  (AbsVal `  w ) }
Colors of variables: wff setvar class
This definition is referenced by:  isnrg  21042
  Copyright terms: Public domain W3C validator