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 
|- .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 eqtr2id 
 |-  ( ( 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. ) )