Metamath Proof Explorer


Theorem nmfval0

Description: The value of the norm function on a structure containing a zero as the distance restricted to the elements of the base set to zero. Examples of structures containing a "zero" are groups (see nmfval2 proved from this theorem and grpidcl ) or more generally monoids (see mndidcl ), or pointed sets). (Contributed by Mario Carneiro, 2-Oct-2015) Extract this result from the proof of nmfval2 . (Revised by BJ, 27-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 nmfval0.n N = norm W
2 nmfval0.x X = Base W
3 nmfval0.z 0 ˙ = 0 W
4 nmfval0.d D = dist W
5 nmfval0.e E = D X × X
6 1 2 3 4 nmfval N = x X x D 0 ˙
7 5 oveqi x E 0 ˙ = x D X × X 0 ˙
8 ovres x X 0 ˙ X x D X × X 0 ˙ = x D 0 ˙
9 8 ancoms 0 ˙ X x X x D X × X 0 ˙ = x D 0 ˙
10 7 9 eqtr2id 0 ˙ X x X x D 0 ˙ = x E 0 ˙
11 10 mpteq2dva 0 ˙ X x X x D 0 ˙ = x X x E 0 ˙
12 6 11 eqtrid 0 ˙ X N = x X x E 0 ˙