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 e. _V |-> ( x e. ( Base ` w ) |-> ( x ( dist ` w ) ( 0g ` w ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnm	|- norm
1		vw	|- w
2		cvv	|- _V
3		vx	|- x
4		cbs	|- Base
5	1	cv	|- w
6	5 4	cfv	|- ( Base ` w )
7	3	cv	|- x
8		cds	|- dist
9	5 8	cfv	|- ( dist ` w )
10		c0g	|- 0g
11	5 10	cfv	|- ( 0g ` w )
12	7 11 9	co	|- ( x ( dist ` w ) ( 0g ` w ) )
13	3 6 12	cmpt	|- ( x e. ( Base ` w ) |-> ( x ( dist ` w ) ( 0g ` w ) ) )
14	1 2 13	cmpt	|- ( w e. _V |-> ( x e. ( Base ` w ) |-> ( x ( dist ` w ) ( 0g ` w ) ) ) )
15	0 14	wceq	|- norm = ( w e. _V |-> ( x e. ( Base ` w ) |-> ( x ( dist ` w ) ( 0g ` w ) ) ) )