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 = ( 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	nmfval2	|- ( W e. Grp -> N = ( x e. X |-> ( x 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	2 3	grpidcl	|- ( W e. Grp -> .0. e. X )
7	1 2 3 4 5	nmfval0	|- ( .0. e. X -> N = ( x e. X |-> ( x E .0. ) ) )
8	6 7	syl	|- ( W e. Grp -> N = ( x e. X |-> ( x E .0. ) ) )