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

Metamath Proof Explorer

Theorem nmge0

Description: The norm of a normed group is nonnegative. Second part of Problem 2 of Kreyszig p. 64. (Contributed by NM, 28-Nov-2006) (Revised by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses nmf.x ⊢ X = Base G
nmf.n ⊢ N = norm ⁡ G
Assertion nmge0 ⊢ G ∈ NrmGrp ∧ A ∈ X → 0 ≤ N ⁡ A

Proof

Step Hyp Ref Expression
1 nmf.x ⊢ X = Base G
2 nmf.n ⊢ N = norm ⁡ G
3 ngpgrp ⊢ G ∈ NrmGrp → G ∈ Grp
4 eqid ⊢ 0 G = 0 G
5 1 4 grpidcl ⊢ G ∈ Grp → 0 G ∈ X
6 3 5 syl ⊢ G ∈ NrmGrp → 0 G ∈ X
7 6 adantr ⊢ G ∈ NrmGrp ∧ A ∈ X → 0 G ∈ X
8 ngpxms ⊢ G ∈ NrmGrp → G ∈ ∞MetSp
9 eqid ⊢ dist ⁡ G = dist ⁡ G
10 1 9 xmsge0 ⊢ G ∈ ∞MetSp ∧ A ∈ X ∧ 0 G ∈ X → 0 ≤ A dist ⁡ G 0 G
11 8 10 syl3an1 ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ 0 G ∈ X → 0 ≤ A dist ⁡ G 0 G
12 7 11 mpd3an3 ⊢ G ∈ NrmGrp ∧ A ∈ X → 0 ≤ A dist ⁡ G 0 G
13 2 1 4 9 nmval ⊢ A ∈ X → N ⁡ A = A dist ⁡ G 0 G
14 13 adantl ⊢ G ∈ NrmGrp ∧ A ∈ X → N ⁡ A = A dist ⁡ G 0 G
15 12 14 breqtrrd ⊢ G ∈ NrmGrp ∧ A ∈ X → 0 ≤ N ⁡ A