Theorem nmval2

Description: The value of the norm 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	nmval2	$$⊢\left(W\in \mathrm{Grp}\wedge A\in X\right)\to N\left(A\right)=AE\underset{\dot{}}{0}$$

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	1 2 3 4	nmval	$$⊢A\in X\to N\left(A\right)=AD\underset{\dot{}}{0}$$
7	6	adantl	$$⊢\left(W\in \mathrm{Grp}\wedge A\in X\right)\to N\left(A\right)=AD\underset{\dot{}}{0}$$
8	5	oveqi	$$⊢AE\underset{\dot{}}{0}=A\left({D\upharpoonright }_{\left(X\times X\right)}\right)\underset{\dot{}}{0}$$
9		id	$$⊢A\in X\to A\in X$$
10	2 3	grpidcl	$$⊢W\in \mathrm{Grp}\to \underset{\dot{}}{0}\in X$$
11		ovres	$$⊢\left(A\in X\wedge \underset{\dot{}}{0}\in X\right)\to A\left({D\upharpoonright }_{\left(X\times X\right)}\right)\underset{\dot{}}{0}=AD\underset{\dot{}}{0}$$
12	9 10 11	syl2anr	$$⊢\left(W\in \mathrm{Grp}\wedge A\in X\right)\to A\left({D\upharpoonright }_{\left(X\times X\right)}\right)\underset{\dot{}}{0}=AD\underset{\dot{}}{0}$$
13	8 12	syl5req	$$⊢\left(W\in \mathrm{Grp}\wedge A\in X\right)\to AD\underset{\dot{}}{0}=AE\underset{\dot{}}{0}$$
14	7 13	eqtrd	$$⊢\left(W\in \mathrm{Grp}\wedge A\in X\right)\to N\left(A\right)=AE\underset{\dot{}}{0}$$