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

Metamath Proof Explorer

Theorem nmeq0

Description: The identity is the only element of the group with zero norm. First part of Problem 2 of Kreyszig p. 64. (Contributed by NM, 24-Nov-2006) (Revised by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses nmf.x 
|- X = ( Base ` G )
nmf.n 
|- N = ( norm ` G )
nmeq0.z 
|- .0. = ( 0g ` G )
Assertion nmeq0 
|- ( ( G e. NrmGrp /\ A e. X ) -> ( ( N ` A ) = 0 <-> A = .0. ) )

Proof

Step Hyp Ref Expression
1 nmf.x 
 |-  X = ( Base ` G )
2 nmf.n 
 |-  N = ( norm ` G )
3 nmeq0.z 
 |-  .0. = ( 0g ` G )
4 eqid 
 |-  ( dist ` G ) = ( dist ` G )
5 2 1 3 4 nmval 
 |-  ( A e. X -> ( N ` A ) = ( A ( dist ` G ) .0. ) )
6 5 adantl 
 |-  ( ( G e. NrmGrp /\ A e. X ) -> ( N ` A ) = ( A ( dist ` G ) .0. ) )
7 6 eqeq1d 
 |-  ( ( G e. NrmGrp /\ A e. X ) -> ( ( N ` A ) = 0 <-> ( A ( dist ` G ) .0. ) = 0 ) )
8 ngpgrp 
 |-  ( G e. NrmGrp -> G e. Grp )
9 8 adantr 
 |-  ( ( G e. NrmGrp /\ A e. X ) -> G e. Grp )
10 1 3 grpidcl 
 |-  ( G e. Grp -> .0. e. X )
11 9 10 syl 
 |-  ( ( G e. NrmGrp /\ A e. X ) -> .0. e. X )
12 ngpxms 
 |-  ( G e. NrmGrp -> G e. *MetSp )
13 1 4 xmseq0 
 |-  ( ( G e. *MetSp /\ A e. X /\ .0. e. X ) -> ( ( A ( dist ` G ) .0. ) = 0 <-> A = .0. ) )
14 12 13 syl3an1 
 |-  ( ( G e. NrmGrp /\ A e. X /\ .0. e. X ) -> ( ( A ( dist ` G ) .0. ) = 0 <-> A = .0. ) )
15 11 14 mpd3an3 
 |-  ( ( G e. NrmGrp /\ A e. X ) -> ( ( A ( dist ` G ) .0. ) = 0 <-> A = .0. ) )
16 7 15 bitrd 
 |-  ( ( G e. NrmGrp /\ A e. X ) -> ( ( N ` A ) = 0 <-> A = .0. ) )