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 ) ) )