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 ˙ = 0 G
Assertion nmeq0 ⊢ G ∈ NrmGrp ∧ A ∈ 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 ˙ = 0 G
4 eqid ⊢ dist ⁡ G = dist ⁡ G
5 2 1 3 4 nmval ⊢ A ∈ X → N ⁡ A = A dist ⁡ G 0 ˙
6 5 adantl ⊢ G ∈ NrmGrp ∧ A ∈ X → N ⁡ A = A dist ⁡ G 0 ˙
7 6 eqeq1d ⊢ G ∈ NrmGrp ∧ A ∈ X → N ⁡ A = 0 ↔ A dist ⁡ G 0 ˙ = 0
8 ngpgrp ⊢ G ∈ NrmGrp → G ∈ Grp
9 8 adantr ⊢ G ∈ NrmGrp ∧ A ∈ X → G ∈ Grp
10 1 3 grpidcl ⊢ G ∈ Grp → 0 ˙ ∈ X
11 9 10 syl ⊢ G ∈ NrmGrp ∧ A ∈ X → 0 ˙ ∈ X
12 ngpxms ⊢ G ∈ NrmGrp → G ∈ ∞MetSp
13 1 4 xmseq0 ⊢ G ∈ ∞MetSp ∧ A ∈ X ∧ 0 ˙ ∈ X → A dist ⁡ G 0 ˙ = 0 ↔ A = 0 ˙
14 12 13 syl3an1 ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ 0 ˙ ∈ X → A dist ⁡ G 0 ˙ = 0 ↔ A = 0 ˙
15 11 14 mpd3an3 ⊢ G ∈ NrmGrp ∧ A ∈ X → A dist ⁡ G 0 ˙ = 0 ↔ A = 0 ˙
16 7 15 bitrd ⊢ G ∈ NrmGrp ∧ A ∈ X → N ⁡ A = 0 ↔ A = 0 ˙