Metamath Proof Explorer

Theorem nmmtri

Description: The triangle inequality for the norm of a subtraction. (Contributed by NM, 27-Dec-2007) (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 nmmtri 
|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` ( A .- B ) ) <_ ( ( N ` A ) + ( N ` B ) ) )

Proof

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