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

Metamath Proof Explorer

Theorem nmrtri

Description: Reverse triangle inequality for the norm of a subtraction. Problem 3 of Kreyszig p. 64. (Contributed by NM, 4-Dec-2006) (Revised by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses nmf.x 
|- X = ( Base ` G )
nmf.n 
|- N = ( norm ` G )
nmmtri.m 
|- .- = ( -g ` G )
Assertion nmrtri 
|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( abs ` ( ( N ` A ) - ( N ` B ) ) ) <_ ( N ` ( A .- B ) ) )

Proof

Step Hyp Ref Expression
1 nmf.x 
 |-  X = ( Base ` G )
2 nmf.n 
 |-  N = ( norm ` G )
3 nmmtri.m 
 |-  .- = ( -g ` G )
4 ngpms 
 |-  ( G e. NrmGrp -> G e. MetSp )
5 4 3ad2ant1 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> G e. MetSp )
6 simp2 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> A e. X )
7 simp3 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> B e. X )
8 ngpgrp 
 |-  ( G e. NrmGrp -> G e. Grp )
9 8 3ad2ant1 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> G e. Grp )
10 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
11 1 10 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. X )
12 9 11 syl 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( 0g ` G ) e. X )
13 eqid 
 |-  ( dist ` G ) = ( dist ` G )
14 1 13 msrtri 
 |-  ( ( G e. MetSp /\ ( A e. X /\ B e. X /\ ( 0g ` G ) e. X ) ) -> ( abs ` ( ( A ( dist ` G ) ( 0g ` G ) ) - ( B ( dist ` G ) ( 0g ` G ) ) ) ) <_ ( A ( dist ` G ) B ) )
15 5 6 7 12 14 syl13anc 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( abs ` ( ( A ( dist ` G ) ( 0g ` G ) ) - ( B ( dist ` G ) ( 0g ` G ) ) ) ) <_ ( A ( dist ` G ) B ) )
16 2 1 10 13 nmval 
 |-  ( A e. X -> ( N ` A ) = ( A ( dist ` G ) ( 0g ` G ) ) )
17 16 3ad2ant2 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` A ) = ( A ( dist ` G ) ( 0g ` G ) ) )
18 2 1 10 13 nmval 
 |-  ( B e. X -> ( N ` B ) = ( B ( dist ` G ) ( 0g ` G ) ) )
19 18 3ad2ant3 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` B ) = ( B ( dist ` G ) ( 0g ` G ) ) )
20 17 19 oveq12d 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( ( N ` A ) - ( N ` B ) ) = ( ( A ( dist ` G ) ( 0g ` G ) ) - ( B ( dist ` G ) ( 0g ` G ) ) ) )
21 20 fveq2d 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( abs ` ( ( N ` A ) - ( N ` B ) ) ) = ( abs ` ( ( A ( dist ` G ) ( 0g ` G ) ) - ( B ( dist ` G ) ( 0g ` G ) ) ) ) )
22 2 1 3 13 ngpds 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A ( dist ` G ) B ) = ( N ` ( A .- B ) ) )
23 22 eqcomd 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` ( A .- B ) ) = ( A ( dist ` G ) B ) )
24 15 21 23 3brtr4d 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( abs ` ( ( N ` A ) - ( N ` B ) ) ) <_ ( N ` ( A .- B ) ) )