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

Metamath Proof Explorer

Theorem nmtri

Description: The triangle inequality for the norm of a sum. (Contributed by NM, 11-Nov-2006) (Revised by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses nmf.x 
|- X = ( Base ` G )
nmf.n 
|- N = ( norm ` G )
nmtri.p 
|- .+ = ( +g ` G )
Assertion nmtri 
|- ( ( 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 nmtri.p 
 |-  .+ = ( +g ` G )
4 ngpgrp 
 |-  ( G e. NrmGrp -> G e. Grp )
5 4 3ad2ant1 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> G e. Grp )
6 simp3 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> B e. X )
7 eqid 
 |-  ( invg ` G ) = ( invg ` G )
8 1 7 grpinvcl 
 |-  ( ( G e. Grp /\ B e. X ) -> ( ( invg ` G ) ` B ) e. X )
9 5 6 8 syl2anc 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( ( invg ` G ) ` B ) e. X )
10 eqid 
 |-  ( -g ` G ) = ( -g ` G )
11 1 2 10 nmmtri 
 |-  ( ( G e. NrmGrp /\ A e. X /\ ( ( invg ` G ) ` B ) e. X ) -> ( N ` ( A ( -g ` G ) ( ( invg ` G ) ` B ) ) ) <_ ( ( N ` A ) + ( N ` ( ( invg ` G ) ` B ) ) ) )
12 9 11 syld3an3 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` ( A ( -g ` G ) ( ( invg ` G ) ` B ) ) ) <_ ( ( N ` A ) + ( N ` ( ( invg ` G ) ` B ) ) ) )
13 simp2 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> A e. X )
14 1 3 10 7 5 13 6 grpsubinv 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A ( -g ` G ) ( ( invg ` G ) ` B ) ) = ( A .+ B ) )
15 14 fveq2d 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` ( A ( -g ` G ) ( ( invg ` G ) ` B ) ) ) = ( N ` ( A .+ B ) ) )
16 1 2 7 nminv 
 |-  ( ( G e. NrmGrp /\ B e. X ) -> ( N ` ( ( invg ` G ) ` B ) ) = ( N ` B ) )
17 16 3adant2 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` ( ( invg ` G ) ` B ) ) = ( N ` B ) )
18 17 oveq2d 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( ( N ` A ) + ( N ` ( ( invg ` G ) ` B ) ) ) = ( ( N ` A ) + ( N ` B ) ) )
19 12 15 18 3brtr3d 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` ( A .+ B ) ) <_ ( ( N ` A ) + ( N ` B ) ) )