This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-nm

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
Assertion df-nm ⊢ norm = w ∈ V ⟼ x ∈ Base w ⟼ x dist ⁡ w 0 w

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnm class norm
1 vw setvar w
2 cvv class V
3 vx setvar x
4 cbs class Base
5 1 cv setvar w
6 5 4 cfv class Base w
7 3 cv setvar x
8 cds class dist
9 5 8 cfv class dist ⁡ w
10 c0g class 0 𝑔
11 5 10 cfv class 0 w
12 7 11 9 co class x dist ⁡ w 0 w
13 3 6 12 cmpt class x ∈ Base w ⟼ x dist ⁡ w 0 w
14 1 2 13 cmpt class w ∈ V ⟼ x ∈ Base w ⟼ x dist ⁡ w 0 w
15 0 14 wceq wff norm = w ∈ V ⟼ x ∈ Base w ⟼ x dist ⁡ w 0 w