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
Assertion nmmtri 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 nmmtri.m - ˙ = - G
4 eqid dist G = dist G
5 2 1 3 4 ngpds G NrmGrp A X B X A dist G B = N A - ˙ B
6 ngpms G NrmGrp G MetSp
7 6 3ad2ant1 G NrmGrp A X B X G MetSp
8 simp2 G NrmGrp A X B X A X
9 simp3 G NrmGrp A X B X B X
10 ngpgrp G NrmGrp G Grp
11 eqid 0 G = 0 G
12 1 11 grpidcl G Grp 0 G X
13 10 12 syl G NrmGrp 0 G X
14 13 3ad2ant1 G NrmGrp A X B X 0 G X
15 1 4 mstri3 G MetSp A X B X 0 G X A dist G B A dist G 0 G + B dist G 0 G
16 7 8 9 14 15 syl13anc G NrmGrp A X B X A dist G B A dist G 0 G + B dist G 0 G
17 2 1 11 4 nmval A X N A = A dist G 0 G
18 17 3ad2ant2 G NrmGrp A X B X N A = A dist G 0 G
19 2 1 11 4 nmval B X N B = B dist G 0 G
20 19 3ad2ant3 G NrmGrp A X B X N B = B dist G 0 G
21 18 20 oveq12d G NrmGrp A X B X N A + N B = A dist G 0 G + B dist G 0 G
22 16 21 breqtrrd G NrmGrp A X B X A dist G B N A + N B
23 5 22 eqbrtrrd G NrmGrp A X B X N A - ˙ B N A + N B