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

Definition df-nrg 18635
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 18629 . 2  class NrmRing
2 vw . . . . . 6  set  w
32cv 1652 . . . . 5  class  w
4 cnm 18626 . . . . 5  class  norm
53, 4cfv 5456 . . . 4  class  ( norm `  w )
6 cabv 15906 . . . . 5  class AbsVal
73, 6cfv 5456 . . . 4  class  (AbsVal `  w )
85, 7wcel 1726 . . 3  wff  ( norm `  w )  e.  (AbsVal `  w )
9 cngp 18627 . . 3  class NrmGrp
108, 2, 9crab 2711 . 2  class  { w  e. NrmGrp  |  ( norm `  w
)  e.  (AbsVal `  w ) }
111, 10wceq 1653 1  wff NrmRing  =  {
w  e. NrmGrp  |  ( norm `  w )  e.  (AbsVal `  w ) }
Colors of variables: wff set class
This definition is referenced by:  isnrg  18698
  Copyright terms: Public domain W3C validator