This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = norm (W)$
		nmfval2.x	$⊢ X = {Base}_{W}$
		nmfval2.z	$⊢ \underset{˙}{0} = 0_{W}$
		nmfval2.d	$⊢ D = dist (W)$
		nmfval2.e	$⊢ E = {D ↾}_{(X \times X)}$
	Assertion	nmval2	$⊢ (W \in Grp \land A \in X) \to N (A) = A E \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		nmfval2.n	$⊢ N = norm (W)$
2		nmfval2.x	$⊢ X = {Base}_{W}$
3		nmfval2.z	$⊢ \underset{˙}{0} = 0_{W}$
4		nmfval2.d	$⊢ D = dist (W)$
5		nmfval2.e	$⊢ E = {D ↾}_{(X \times X)}$
6	1 2 3 4	nmval	$⊢ A \in X \to N (A) = A D \underset{˙}{0}$
7	6	adantl	$⊢ (W \in Grp \land A \in X) \to N (A) = A D \underset{˙}{0}$
8	5	oveqi	$⊢ A E \underset{˙}{0} = A ({D ↾}_{(X \times X)}) \underset{˙}{0}$
9		id	$⊢ A \in X \to A \in X$
10	2 3	grpidcl	$⊢ W \in Grp \to \underset{˙}{0} \in X$
11		ovres	$⊢ (A \in X \land \underset{˙}{0} \in X) \to A ({D ↾}_{(X \times X)}) \underset{˙}{0} = A D \underset{˙}{0}$
12	9 10 11	syl2anr	$⊢ (W \in Grp \land A \in X) \to A ({D ↾}_{(X \times X)}) \underset{˙}{0} = A D \underset{˙}{0}$
13	8 12	eqtr2id	$⊢ (W \in Grp \land A \in X) \to A D \underset{˙}{0} = A E \underset{˙}{0}$
14	7 13	eqtrd	$⊢ (W \in Grp \land A \in X) \to N (A) = A E \underset{˙}{0}$