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 e. NrmGrp /\ A e. X ) -> 0 <_ ( N ` A ) )

Proof

Step Hyp Ref Expression
1 nmf.x 
 |-  X = ( Base ` G )
2 nmf.n 
 |-  N = ( norm ` G )
3 ngpgrp 
 |-  ( G e. NrmGrp -> G e. Grp )
4 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
5 1 4 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. X )
6 3 5 syl 
 |-  ( G e. NrmGrp -> ( 0g ` G ) e. X )
7 6 adantr 
 |-  ( ( G e. NrmGrp /\ A e. X ) -> ( 0g ` G ) e. X )
8 ngpxms 
 |-  ( G e. NrmGrp -> G e. *MetSp )
9 eqid 
 |-  ( dist ` G ) = ( dist ` G )
10 1 9 xmsge0 
 |-  ( ( G e. *MetSp /\ A e. X /\ ( 0g ` G ) e. X ) -> 0 <_ ( A ( dist ` G ) ( 0g ` G ) ) )
11 8 10 syl3an1 
 |-  ( ( G e. NrmGrp /\ A e. X /\ ( 0g ` G ) e. X ) -> 0 <_ ( A ( dist ` G ) ( 0g ` G ) ) )
12 7 11 mpd3an3 
 |-  ( ( G e. NrmGrp /\ A e. X ) -> 0 <_ ( A ( dist ` G ) ( 0g ` G ) ) )
13 2 1 4 9 nmval 
 |-  ( A e. X -> ( N ` A ) = ( A ( dist ` G ) ( 0g ` G ) ) )
14 13 adantl 
 |-  ( ( G e. NrmGrp /\ A e. X ) -> ( N ` A ) = ( A ( dist ` G ) ( 0g ` G ) ) )
15 12 14 breqtrrd 
 |-  ( ( G e. NrmGrp /\ A e. X ) -> 0 <_ ( N ` A ) )