Metamath Proof Explorer


Theorem nmfval2

Description: The value of the norm function on a group as the distance restricted to the elements of the base set to zero. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses nmfval2.n 𝑁 = ( norm ‘ 𝑊 )
nmfval2.x 𝑋 = ( Base ‘ 𝑊 )
nmfval2.z 0 = ( 0g𝑊 )
nmfval2.d 𝐷 = ( dist ‘ 𝑊 )
nmfval2.e 𝐸 = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) )
Assertion nmfval2 ( 𝑊 ∈ Grp → 𝑁 = ( 𝑥𝑋 ↦ ( 𝑥 𝐸 0 ) ) )

Proof

Step Hyp Ref Expression
1 nmfval2.n 𝑁 = ( norm ‘ 𝑊 )
2 nmfval2.x 𝑋 = ( Base ‘ 𝑊 )
3 nmfval2.z 0 = ( 0g𝑊 )
4 nmfval2.d 𝐷 = ( dist ‘ 𝑊 )
5 nmfval2.e 𝐸 = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) )
6 2 3 grpidcl ( 𝑊 ∈ Grp → 0𝑋 )
7 1 2 3 4 5 nmfval0 ( 0𝑋𝑁 = ( 𝑥𝑋 ↦ ( 𝑥 𝐸 0 ) ) )
8 6 7 syl ( 𝑊 ∈ Grp → 𝑁 = ( 𝑥𝑋 ↦ ( 𝑥 𝐸 0 ) ) )