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 24504
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 24498 . 2 class norm
2 vw . . 3 setvar 𝑀
3 cvv 3471 . . 3 class V
4 vx . . . 4 setvar π‘₯
52cv 1533 . . . . 5 class 𝑀
6 cbs 17180 . . . . 5 class Base
75, 6cfv 6548 . . . 4 class (Baseβ€˜π‘€)
84cv 1533 . . . . 5 class π‘₯
9 c0g 17421 . . . . . 6 class 0g
105, 9cfv 6548 . . . . 5 class (0gβ€˜π‘€)
11 cds 17242 . . . . . 6 class dist
125, 11cfv 6548 . . . . 5 class (distβ€˜π‘€)
138, 10, 12co 7420 . . . 4 class (π‘₯(distβ€˜π‘€)(0gβ€˜π‘€))
144, 7, 13cmpt 5231 . . 3 class (π‘₯ ∈ (Baseβ€˜π‘€) ↦ (π‘₯(distβ€˜π‘€)(0gβ€˜π‘€)))
152, 3, 14cmpt 5231 . 2 class (𝑀 ∈ V ↦ (π‘₯ ∈ (Baseβ€˜π‘€) ↦ (π‘₯(distβ€˜π‘€)(0gβ€˜π‘€))))
161, 15wceq 1534 1 wff norm = (𝑀 ∈ V ↦ (π‘₯ ∈ (Baseβ€˜π‘€) ↦ (π‘₯(distβ€˜π‘€)(0gβ€˜π‘€))))
Colors of variables: wff setvar class
This definition is referenced by:  nmfval  24510
  Copyright terms: Public domain W3C validator