Metamath Proof Explorer

Theorem nmrtri

Description: Reverse triangle inequality for the norm of a subtraction. Problem 3 of Kreyszig p. 64. (Contributed by NM, 4-Dec-2006) (Revised by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses nmf.x ⊢ X = Base G
nmf.n ⊢ N = norm ⁡ G
nmmtri.m ⊢ - ˙ = - G
Assertion nmrtri ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X → N ⁡ A − N ⁡ B ≤ N ⁡ A - ˙ B

Proof

Step Hyp Ref Expression
1 nmf.x ⊢ X = Base G
2 nmf.n ⊢ N = norm ⁡ G
3 nmmtri.m ⊢ - ˙ = - G
4 ngpms ⊢ G ∈ NrmGrp → G ∈ MetSp
5 4 3ad2ant1 ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X → G ∈ MetSp
6 simp2 ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X → A ∈ X
7 simp3 ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X → B ∈ X
8 ngpgrp ⊢ G ∈ NrmGrp → G ∈ Grp
9 8 3ad2ant1 ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X → G ∈ Grp
10 eqid ⊢ 0 G = 0 G
11 1 10 grpidcl ⊢ G ∈ Grp → 0 G ∈ X
12 9 11 syl ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X → 0 G ∈ X
13 eqid ⊢ dist ⁡ G = dist ⁡ G
14 1 13 msrtri ⊢ G ∈ MetSp ∧ A ∈ X ∧ B ∈ X ∧ 0 G ∈ X → A dist ⁡ G 0 G − B dist ⁡ G 0 G ≤ A dist ⁡ G B
15 5 6 7 12 14 syl13anc ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X → A dist ⁡ G 0 G − B dist ⁡ G 0 G ≤ A dist ⁡ G B
16 2 1 10 13 nmval ⊢ A ∈ X → N ⁡ A = A dist ⁡ G 0 G
17 16 3ad2ant2 ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X → N ⁡ A = A dist ⁡ G 0 G
18 2 1 10 13 nmval ⊢ B ∈ X → N ⁡ B = B dist ⁡ G 0 G
19 18 3ad2ant3 ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X → N ⁡ B = B dist ⁡ G 0 G
20 17 19 oveq12d ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X → N ⁡ A − N ⁡ B = A dist ⁡ G 0 G − B dist ⁡ G 0 G
21 20 fveq2d ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X → N ⁡ A − N ⁡ B = A dist ⁡ G 0 G − B dist ⁡ G 0 G
22 2 1 3 13 ngpds ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X → A dist ⁡ G B = N ⁡ A - ˙ B
23 22 eqcomd ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X → N ⁡ A - ˙ B = A dist ⁡ G B
24 15 21 23 3brtr4d ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X → N ⁡ A − N ⁡ B ≤ N ⁡ A - ˙ B