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	$⊢ \underset{˙}{0} = 0_{W}$
	nmfval0.d	$⊢ D = dist (W)$
	nmfval0.e	$⊢ E = {D ↾}_{(X \times X)}$
Assertion	nmfval0	$⊢ \underset{˙}{0} \in X \to N = (x \in X ⟼ x E \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		nmfval0.n	$⊢ N = norm (W)$
2		nmfval0.x	$⊢ X = {Base}_{W}$
3		nmfval0.z	$⊢ \underset{˙}{0} = 0_{W}$
4		nmfval0.d	$⊢ D = dist (W)$
5		nmfval0.e	$⊢ E = {D ↾}_{(X \times X)}$
6	1 2 3 4	nmfval	$⊢ N = (x \in X ⟼ x D \underset{˙}{0})$
7	5	oveqi	$⊢ x E \underset{˙}{0} = x ({D ↾}_{(X \times X)}) \underset{˙}{0}$
8		ovres	$⊢ (x \in X \land \underset{˙}{0} \in X) \to x ({D ↾}_{(X \times X)}) \underset{˙}{0} = x D \underset{˙}{0}$
9	8	ancoms	$⊢ (\underset{˙}{0} \in X \land x \in X) \to x ({D ↾}_{(X \times X)}) \underset{˙}{0} = x D \underset{˙}{0}$
10	7 9	eqtr2id	$⊢ (\underset{˙}{0} \in X \land x \in X) \to x D \underset{˙}{0} = x E \underset{˙}{0}$
11	10	mpteq2dva	$⊢ \underset{˙}{0} \in X \to (x \in X ⟼ x D \underset{˙}{0}) = (x \in X ⟼ x E \underset{˙}{0})$
12	6 11	eqtrid	$⊢ \underset{˙}{0} \in X \to N = (x \in X ⟼ x E \underset{˙}{0})$

Metamath Proof Explorer

Theorem nmfval0

Proof