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	$$⊢\mathrm{norm}=\left(w\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_w⟼x\mathrm{dist}\left(w\right)0_w\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnm	$$class\mathrm{norm}$$
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarw$$
6	5 4	cfv	$$class{\mathrm{Base}}_w$$
7	3	cv	$$setvarx$$
8		cds	$$class\mathrm{dist}$$
9	5 8	cfv	$$class\mathrm{dist}\left(w\right)$$
10		c0g	$$class{0}_{𝑔}$$
11	5 10	cfv	$$class{0}_w$$
12	7 11 9	co	$$class\left(x\mathrm{dist}\left(w\right)0_w\right)$$
13	3 6 12	cmpt	$$class\left(x\in {\mathrm{Base}}_w⟼x\mathrm{dist}\left(w\right)0_w\right)$$
14	1 2 13	cmpt	$$class\left(w\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_w⟼x\mathrm{dist}\left(w\right)0_w\right)\right)$$
15	0 14	wceq	$$wff\mathrm{norm}=\left(w\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_w⟼x\mathrm{dist}\left(w\right)0_w\right)\right)$$