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 = ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( 𝑥 ( dist ‘ 𝑤 ) ( 0g ‘ 𝑤 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnm	⊢ norm
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5	1	cv	⊢ 𝑤
6	5 4	cfv	⊢ ( Base ‘ 𝑤 )
7	3	cv	⊢ 𝑥
8		cds	⊢ dist
9	5 8	cfv	⊢ ( dist ‘ 𝑤 )
10		c0g	⊢ 0g
11	5 10	cfv	⊢ ( 0g ‘ 𝑤 )
12	7 11 9	co	⊢ ( 𝑥 ( dist ‘ 𝑤 ) ( 0g ‘ 𝑤 ) )
13	3 6 12	cmpt	⊢ ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( 𝑥 ( dist ‘ 𝑤 ) ( 0g ‘ 𝑤 ) ) )
14	1 2 13	cmpt	⊢ ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( 𝑥 ( dist ‘ 𝑤 ) ( 0g ‘ 𝑤 ) ) ) )
15	0 14	wceq	⊢ norm = ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( 𝑥 ( dist ‘ 𝑤 ) ( 0g ‘ 𝑤 ) ) ) )