MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nm Structured version   Visualization version   GIF version

Definition df-nm 22434
Description: Define the norm on a group or ring (when it makes sense) in terms of the distance to zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
Assertion
Ref Expression
df-nm norm = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤) ↦ (𝑥(dist‘𝑤)(0g𝑤))))
Distinct variable group:   𝑥,𝑤

Detailed syntax breakdown of Definition df-nm
StepHypRef Expression
1 cnm 22428 . 2 class norm
2 vw . . 3 setvar 𝑤
3 cvv 3231 . . 3 class V
4 vx . . . 4 setvar 𝑥
52cv 1522 . . . . 5 class 𝑤
6 cbs 15904 . . . . 5 class Base
75, 6cfv 5926 . . . 4 class (Base‘𝑤)
84cv 1522 . . . . 5 class 𝑥
9 c0g 16147 . . . . . 6 class 0g
105, 9cfv 5926 . . . . 5 class (0g𝑤)
11 cds 15997 . . . . . 6 class dist
125, 11cfv 5926 . . . . 5 class (dist‘𝑤)
138, 10, 12co 6690 . . . 4 class (𝑥(dist‘𝑤)(0g𝑤))
144, 7, 13cmpt 4762 . . 3 class (𝑥 ∈ (Base‘𝑤) ↦ (𝑥(dist‘𝑤)(0g𝑤)))
152, 3, 14cmpt 4762 . 2 class (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤) ↦ (𝑥(dist‘𝑤)(0g𝑤))))
161, 15wceq 1523 1 wff norm = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤) ↦ (𝑥(dist‘𝑤)(0g𝑤))))
Colors of variables: wff setvar class
This definition is referenced by:  nmfval  22440
  Copyright terms: Public domain W3C validator