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