Theorem nmfval2

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

Proof

Step	Hyp	Ref	Expression
1		nmfval2.n	$$⊢N=\mathrm{norm}\left(W\right)$$
2		nmfval2.x	$$⊢X={\mathrm{Base}}_W$$
3		nmfval2.z	$$⊢\underset{\dot{}}{0}=0_W$$
4		nmfval2.d	$$⊢D=\mathrm{dist}\left(W\right)$$
5		nmfval2.e	$$⊢E={D\upharpoonright }_{\left(X\times X\right)}$$
6	2 3	grpidcl	$$⊢W\in \mathrm{Grp}\to \underset{\dot{}}{0}\in X$$
7	1 2 3 4 5	nmfval0	$$⊢\underset{\dot{}}{0}\in X\to N=\left(x\in X⟼xE\underset{\dot{}}{0}\right)$$
8	6 7	syl	$$⊢W\in \mathrm{Grp}\to N=\left(x\in X⟼xE\underset{\dot{}}{0}\right)$$