Metamath Proof Explorer


Theorem nmval2

Description: The value of the norm 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 nmval2 W Grp A X N A = A 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 1 2 3 4 nmval A X N A = A D 0 ˙
7 6 adantl W Grp A X N A = A D 0 ˙
8 5 oveqi A E 0 ˙ = A D X × X 0 ˙
9 id A X A X
10 2 3 grpidcl W Grp 0 ˙ X
11 ovres A X 0 ˙ X A D X × X 0 ˙ = A D 0 ˙
12 9 10 11 syl2anr W Grp A X A D X × X 0 ˙ = A D 0 ˙
13 8 12 eqtr2id W Grp A X A D 0 ˙ = A E 0 ˙
14 7 13 eqtrd W Grp A X N A = A E 0 ˙