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	|- .0. = ( 0g ` W )
	nmfval2.d	|- D = ( dist ` W )
	nmfval2.e	|- E = ( D |` ( X X. X ) )
Assertion	nmval2	|- ( ( W e. Grp /\ A e. X ) -> ( N ` A ) = ( A E .0. ) )

Proof

Step	Hyp	Ref	Expression
1		nmfval2.n	|- N = ( norm ` W )
2		nmfval2.x	|- X = ( Base ` W )
3		nmfval2.z	|- .0. = ( 0g ` W )
4		nmfval2.d	|- D = ( dist ` W )
5		nmfval2.e	|- E = ( D |` ( X X. X ) )
6	1 2 3 4	nmval	|- ( A e. X -> ( N ` A ) = ( A D .0. ) )
7	6	adantl	|- ( ( W e. Grp /\ A e. X ) -> ( N ` A ) = ( A D .0. ) )
8	5	oveqi	|- ( A E .0. ) = ( A ( D |` ( X X. X ) ) .0. )
9		id	|- ( A e. X -> A e. X )
10	2 3	grpidcl	|- ( W e. Grp -> .0. e. X )
11		ovres	|- ( ( A e. X /\ .0. e. X ) -> ( A ( D |` ( X X. X ) ) .0. ) = ( A D .0. ) )
12	9 10 11	syl2anr	|- ( ( W e. Grp /\ A e. X ) -> ( A ( D |` ( X X. X ) ) .0. ) = ( A D .0. ) )
13	8 12	syl5req	|- ( ( W e. Grp /\ A e. X ) -> ( A D .0. ) = ( A E .0. ) )
14	7 13	eqtrd	|- ( ( W e. Grp /\ A e. X ) -> ( N ` A ) = ( A E .0. ) )