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

Definition df-nrg 18108
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 18102 . 2  class NrmRing
2 vw . . . . . 6  set  w
32cv 1622 . . . . 5  class  w
4 cnm 18099 . . . . 5  class  norm
53, 4cfv 5255 . . . 4  class  ( norm `  w )
6 cabv 15581 . . . . 5  class AbsVal
73, 6cfv 5255 . . . 4  class  (AbsVal `  w )
85, 7wcel 1684 . . 3  wff  ( norm `  w )  e.  (AbsVal `  w )
9 cngp 18100 . . 3  class NrmGrp
108, 2, 9crab 2547 . 2  class  { w  e. NrmGrp  |  ( norm `  w
)  e.  (AbsVal `  w ) }
111, 10wceq 1623 1  wff NrmRing  =  {
w  e. NrmGrp  |  ( norm `  w )  e.  (AbsVal `  w ) }
Colors of variables: wff set class
This definition is referenced by:  isnrg  18171
  Copyright terms: Public domain W3C validator