Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-nm | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-nm | ⊢ norm = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤) ↦ (𝑥(dist‘𝑤)(0g‘𝑤)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnm 23428 | . 2 class norm | |
2 | vw | . . 3 setvar 𝑤 | |
3 | cvv 3398 | . . 3 class V | |
4 | vx | . . . 4 setvar 𝑥 | |
5 | 2 | cv 1542 | . . . . 5 class 𝑤 |
6 | cbs 16666 | . . . . 5 class Base | |
7 | 5, 6 | cfv 6358 | . . . 4 class (Base‘𝑤) |
8 | 4 | cv 1542 | . . . . 5 class 𝑥 |
9 | c0g 16898 | . . . . . 6 class 0g | |
10 | 5, 9 | cfv 6358 | . . . . 5 class (0g‘𝑤) |
11 | cds 16758 | . . . . . 6 class dist | |
12 | 5, 11 | cfv 6358 | . . . . 5 class (dist‘𝑤) |
13 | 8, 10, 12 | co 7191 | . . . 4 class (𝑥(dist‘𝑤)(0g‘𝑤)) |
14 | 4, 7, 13 | cmpt 5120 | . . 3 class (𝑥 ∈ (Base‘𝑤) ↦ (𝑥(dist‘𝑤)(0g‘𝑤))) |
15 | 2, 3, 14 | cmpt 5120 | . 2 class (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤) ↦ (𝑥(dist‘𝑤)(0g‘𝑤)))) |
16 | 1, 15 | wceq 1543 | 1 wff norm = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤) ↦ (𝑥(dist‘𝑤)(0g‘𝑤)))) |
Colors of variables: wff setvar class |
This definition is referenced by: nmfval 23440 |
Copyright terms: Public domain | W3C validator |