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
Assertion nmtri2 G NrmGrp A X B X C 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
4 ngpgrp G NrmGrp G Grp
5 eqid + G = + G
6 1 5 3 grpnpncan G Grp A X B X C X A - ˙ B + G B - ˙ C = A - ˙ C
7 6 eqcomd G Grp A X B X C X A - ˙ C = A - ˙ B + G B - ˙ C
8 4 7 sylan G NrmGrp A X B X C X A - ˙ C = A - ˙ B + G B - ˙ C
9 8 fveq2d G NrmGrp A X B X C X N A - ˙ C = N A - ˙ B + G B - ˙ C
10 simpl G NrmGrp A X B X C X G NrmGrp
11 4 adantr G NrmGrp A X B X C X G Grp
12 simpr1 G NrmGrp A X B X C X A X
13 simpr2 G NrmGrp A X B X C X B X
14 1 3 grpsubcl G Grp A X B X A - ˙ B X
15 11 12 13 14 syl3anc G NrmGrp A X B X C X A - ˙ B X
16 simpr3 G NrmGrp A X B X C X C X
17 1 3 grpsubcl G Grp B X C X B - ˙ C X
18 11 13 16 17 syl3anc G NrmGrp A X B X C X B - ˙ C X
19 1 2 5 nmtri G NrmGrp A - ˙ B X B - ˙ C X N A - ˙ B + G B - ˙ C N A - ˙ B + N B - ˙ C
20 10 15 18 19 syl3anc G NrmGrp A X B X C X N A - ˙ B + G B - ˙ C N A - ˙ B + N B - ˙ C
21 9 20 eqbrtrd G NrmGrp A X B X C X N A - ˙ C N A - ˙ B + N B - ˙ C