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

Metamath Proof Explorer

Theorem nmtri2

Description: Triangle inequality for the norm of two subtractions. (Contributed by NM, 24-Feb-2008) (Revised by AV, 8-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 nmtri2.x 
 |-  X = ( Base ` G )
2 nmtri2.n 
 |-  N = ( norm ` G )
3 nmtri2.m 
 |-  .- = ( -g ` G )
4 ngpgrp 
 |-  ( G e. NrmGrp -> G e. Grp )
5 eqid 
 |-  ( +g ` G ) = ( +g ` G )
6 1 5 3 grpnpncan 
 |-  ( ( G e. Grp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A .- B ) ( +g ` G ) ( B .- C ) ) = ( A .- C ) )
7 6 eqcomd 
 |-  ( ( G e. Grp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A .- C ) = ( ( A .- B ) ( +g ` G ) ( B .- C ) ) )
8 4 7 sylan 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A .- C ) = ( ( A .- B ) ( +g ` G ) ( B .- C ) ) )
9 8 fveq2d 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( N ` ( A .- C ) ) = ( N ` ( ( A .- B ) ( +g ` G ) ( B .- C ) ) ) )
10 simpl 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> G e. NrmGrp )
11 4 adantr 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> G e. Grp )
12 simpr1 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> A e. X )
13 simpr2 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> B e. X )
14 1 3 grpsubcl 
 |-  ( ( G e. Grp /\ A e. X /\ B e. X ) -> ( A .- B ) e. X )
15 11 12 13 14 syl3anc 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A .- B ) e. X )
16 simpr3 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> C e. X )
17 1 3 grpsubcl 
 |-  ( ( G e. Grp /\ B e. X /\ C e. X ) -> ( B .- C ) e. X )
18 11 13 16 17 syl3anc 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( B .- C ) e. X )
19 1 2 5 nmtri 
 |-  ( ( G e. NrmGrp /\ ( A .- B ) e. X /\ ( B .- C ) e. X ) -> ( N ` ( ( A .- B ) ( +g ` G ) ( B .- C ) ) ) <_ ( ( N ` ( A .- B ) ) + ( N ` ( B .- C ) ) ) )
20 10 15 18 19 syl3anc 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( N ` ( ( A .- B ) ( +g ` G ) ( B .- C ) ) ) <_ ( ( N ` ( A .- B ) ) + ( N ` ( B .- C ) ) ) )
21 9 20 eqbrtrd 
 |-  ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( N ` ( A .- C ) ) <_ ( ( N ` ( A .- B ) ) + ( N ` ( B .- C ) ) ) )