# 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}={\mathrm{Base}}_{{G}}$
nmf.n ${⊢}{N}=\mathrm{norm}\left({G}\right)$
Assertion nmge0 ${⊢}\left({G}\in \mathrm{NrmGrp}\wedge {A}\in {X}\right)\to 0\le {N}\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 nmf.x ${⊢}{X}={\mathrm{Base}}_{{G}}$
2 nmf.n ${⊢}{N}=\mathrm{norm}\left({G}\right)$
3 ngpgrp ${⊢}{G}\in \mathrm{NrmGrp}\to {G}\in \mathrm{Grp}$
4 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
5 1 4 grpidcl ${⊢}{G}\in \mathrm{Grp}\to {0}_{{G}}\in {X}$
6 3 5 syl ${⊢}{G}\in \mathrm{NrmGrp}\to {0}_{{G}}\in {X}$
7 6 adantr ${⊢}\left({G}\in \mathrm{NrmGrp}\wedge {A}\in {X}\right)\to {0}_{{G}}\in {X}$
8 ngpxms ${⊢}{G}\in \mathrm{NrmGrp}\to {G}\in \mathrm{\infty MetSp}$
9 eqid ${⊢}\mathrm{dist}\left({G}\right)=\mathrm{dist}\left({G}\right)$
10 1 9 xmsge0 ${⊢}\left({G}\in \mathrm{\infty MetSp}\wedge {A}\in {X}\wedge {0}_{{G}}\in {X}\right)\to 0\le {A}\mathrm{dist}\left({G}\right){0}_{{G}}$
11 8 10 syl3an1 ${⊢}\left({G}\in \mathrm{NrmGrp}\wedge {A}\in {X}\wedge {0}_{{G}}\in {X}\right)\to 0\le {A}\mathrm{dist}\left({G}\right){0}_{{G}}$
12 7 11 mpd3an3 ${⊢}\left({G}\in \mathrm{NrmGrp}\wedge {A}\in {X}\right)\to 0\le {A}\mathrm{dist}\left({G}\right){0}_{{G}}$
13 2 1 4 9 nmval ${⊢}{A}\in {X}\to {N}\left({A}\right)={A}\mathrm{dist}\left({G}\right){0}_{{G}}$
14 13 adantl ${⊢}\left({G}\in \mathrm{NrmGrp}\wedge {A}\in {X}\right)\to {N}\left({A}\right)={A}\mathrm{dist}\left({G}\right){0}_{{G}}$
15 12 14 breqtrrd ${⊢}\left({G}\in \mathrm{NrmGrp}\wedge {A}\in {X}\right)\to 0\le {N}\left({A}\right)$