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
Assertion nmtri G NrmGrp A X B 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
4 ngpgrp G NrmGrp G Grp
5 4 3ad2ant1 G NrmGrp A X B X G Grp
6 simp3 G NrmGrp A X B X B X
7 eqid inv g G = inv g G
8 1 7 grpinvcl G Grp B X inv g G B X
9 5 6 8 syl2anc G NrmGrp A X B X inv g G B X
10 eqid - G = - G
11 1 2 10 nmmtri G NrmGrp A X inv g G B X N A - G inv g G B N A + N inv g G B
12 9 11 syld3an3 G NrmGrp A X B X N A - G inv g G B N A + N inv g G B
13 simp2 G NrmGrp A X B X A X
14 1 3 10 7 5 13 6 grpsubinv G NrmGrp A X B X A - G inv g G B = A + ˙ B
15 14 fveq2d G NrmGrp A X B X N A - G inv g G B = N A + ˙ B
16 1 2 7 nminv G NrmGrp B X N inv g G B = N B
17 16 3adant2 G NrmGrp A X B X N inv g G B = N B
18 17 oveq2d G NrmGrp A X B X N A + N inv g G B = N A + N B
19 12 15 18 3brtr3d G NrmGrp A X B X N A + ˙ B N A + N B