Metamath Proof Explorer


Theorem nmval2

Description: The value of the norm function using a restricted metric. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses nmfval.n N = norm W
nmfval.x X = Base W
nmfval.z 0 ˙ = 0 W
nmfval.d D = dist W
nmfval.e E = D X × X
Assertion nmval2 W Grp A X N A = A E 0 ˙

Proof

Step Hyp Ref Expression
1 nmfval.n N = norm W
2 nmfval.x X = Base W
3 nmfval.z 0 ˙ = 0 W
4 nmfval.d D = dist W
5 nmfval.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 syl5req W Grp A X A D 0 ˙ = A E 0 ˙
14 7 13 eqtrd W Grp A X N A = A E 0 ˙