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 𝑋 = ( Base ‘ 𝐺 )
nmf.n 𝑁 = ( norm ‘ 𝐺 )
nmeq0.z 0 = ( 0g𝐺 )
Assertion nmeq0 ( ( 𝐺 ∈ NrmGrp ∧ 𝐴𝑋 ) → ( ( 𝑁𝐴 ) = 0 ↔ 𝐴 = 0 ) )

Proof

Step Hyp Ref Expression
1 nmf.x 𝑋 = ( Base ‘ 𝐺 )
2 nmf.n 𝑁 = ( norm ‘ 𝐺 )
3 nmeq0.z 0 = ( 0g𝐺 )
4 eqid ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
5 2 1 3 4 nmval ( 𝐴𝑋 → ( 𝑁𝐴 ) = ( 𝐴 ( dist ‘ 𝐺 ) 0 ) )
6 5 adantl ( ( 𝐺 ∈ NrmGrp ∧ 𝐴𝑋 ) → ( 𝑁𝐴 ) = ( 𝐴 ( dist ‘ 𝐺 ) 0 ) )
7 6 eqeq1d ( ( 𝐺 ∈ NrmGrp ∧ 𝐴𝑋 ) → ( ( 𝑁𝐴 ) = 0 ↔ ( 𝐴 ( dist ‘ 𝐺 ) 0 ) = 0 ) )
8 ngpgrp ( 𝐺 ∈ NrmGrp → 𝐺 ∈ Grp )
9 8 adantr ( ( 𝐺 ∈ NrmGrp ∧ 𝐴𝑋 ) → 𝐺 ∈ Grp )
10 1 3 grpidcl ( 𝐺 ∈ Grp → 0𝑋 )
11 9 10 syl ( ( 𝐺 ∈ NrmGrp ∧ 𝐴𝑋 ) → 0𝑋 )
12 ngpxms ( 𝐺 ∈ NrmGrp → 𝐺 ∈ ∞MetSp )
13 1 4 xmseq0 ( ( 𝐺 ∈ ∞MetSp ∧ 𝐴𝑋0𝑋 ) → ( ( 𝐴 ( dist ‘ 𝐺 ) 0 ) = 0 ↔ 𝐴 = 0 ) )
14 12 13 syl3an1 ( ( 𝐺 ∈ NrmGrp ∧ 𝐴𝑋0𝑋 ) → ( ( 𝐴 ( dist ‘ 𝐺 ) 0 ) = 0 ↔ 𝐴 = 0 ) )
15 11 14 mpd3an3 ( ( 𝐺 ∈ NrmGrp ∧ 𝐴𝑋 ) → ( ( 𝐴 ( dist ‘ 𝐺 ) 0 ) = 0 ↔ 𝐴 = 0 ) )
16 7 15 bitrd ( ( 𝐺 ∈ NrmGrp ∧ 𝐴𝑋 ) → ( ( 𝑁𝐴 ) = 0 ↔ 𝐴 = 0 ) )