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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
nmf.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
Assertion nmge0 ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ 𝐴 ) )

Proof

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