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 N = norm W
nmfval2.x X = Base W
nmfval2.z 0 ˙ = 0 W
nmfval2.d D = dist W
nmfval2.e E = D X × X
Assertion nmfval2 W Grp N = x X x E 0 ˙

Proof

Step Hyp Ref Expression
1 nmfval2.n N = norm W
2 nmfval2.x X = Base W
3 nmfval2.z 0 ˙ = 0 W
4 nmfval2.d D = dist W
5 nmfval2.e E = D X × X
6 2 3 grpidcl W Grp 0 ˙ X
7 1 2 3 4 5 nmfval0 0 ˙ X N = x X x E 0 ˙
8 6 7 syl W Grp N = x X x E 0 ˙