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=\mathrm{norm}\left(W\right)$$
	nmfval0.x	$$⊢X={\mathrm{Base}}_W$$
	nmfval0.z	$$⊢\underset{\dot{}}{0}=0_W$$
	nmfval0.d	$$⊢D=\mathrm{dist}\left(W\right)$$
	nmfval0.e	$$⊢E={D\upharpoonright }_{\left(X\times X\right)}$$
Assertion	nmfval0	$$⊢\underset{\dot{}}{0}\in X\to N=\left(x\in X⟼xE\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		nmfval0.n	$$⊢N=\mathrm{norm}\left(W\right)$$
2		nmfval0.x	$$⊢X={\mathrm{Base}}_W$$
3		nmfval0.z	$$⊢\underset{\dot{}}{0}=0_W$$
4		nmfval0.d	$$⊢D=\mathrm{dist}\left(W\right)$$
5		nmfval0.e	$$⊢E={D\upharpoonright }_{\left(X\times X\right)}$$
6	1 2 3 4	nmfval	$$⊢N=\left(x\in X⟼xD\underset{\dot{}}{0}\right)$$
7	5	oveqi	$$⊢xE\underset{\dot{}}{0}=x\left({D\upharpoonright }_{\left(X\times X\right)}\right)\underset{\dot{}}{0}$$
8		ovres	$$⊢\left(x\in X\wedge \underset{\dot{}}{0}\in X\right)\to x\left({D\upharpoonright }_{\left(X\times X\right)}\right)\underset{\dot{}}{0}=xD\underset{\dot{}}{0}$$
9	8	ancoms	$$⊢\left(\underset{\dot{}}{0}\in X\wedge x\in X\right)\to x\left({D\upharpoonright }_{\left(X\times X\right)}\right)\underset{\dot{}}{0}=xD\underset{\dot{}}{0}$$
10	7 9	eqtr2id	$$⊢\left(\underset{\dot{}}{0}\in X\wedge x\in X\right)\to xD\underset{\dot{}}{0}=xE\underset{\dot{}}{0}$$
11	10	mpteq2dva	$$⊢\underset{\dot{}}{0}\in X\to \left(x\in X⟼xD\underset{\dot{}}{0}\right)=\left(x\in X⟼xE\underset{\dot{}}{0}\right)$$
12	6 11	syl5eq	$$⊢\underset{\dot{}}{0}\in X\to N=\left(x\in X⟼xE\underset{\dot{}}{0}\right)$$