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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
nmf.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
nmmtri.m ⊢ − = ( -g ‘ 𝐺 )
Assertion nmrtri ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( abs ‘ ( ( 𝑁 ‘ 𝐴 ) − ( 𝑁 ‘ 𝐵 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 nmf.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 nmf.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
3 nmmtri.m ⊢ − = ( -g ‘ 𝐺 )
4 ngpms ⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp )
5 4 3ad2ant1 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐺 ∈ MetSp )
6 simp2 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
7 simp3 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
8 ngpgrp ⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ Grp )
9 8 3ad2ant1 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐺 ∈ Grp )
10 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
11 1 10 grpidcl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
12 9 11 syl ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
13 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
14 1 13 msrtri ⊢ ( ( 𝐺 ∈ MetSp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑋 ) ) → ( abs ‘ ( ( 𝐴 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) − ( 𝐵 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ) ) ≤ ( 𝐴 ( dist ‘ 𝐺 ) 𝐵 ) )
15 5 6 7 12 14 syl13anc ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( abs ‘ ( ( 𝐴 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) − ( 𝐵 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ) ) ≤ ( 𝐴 ( dist ‘ 𝐺 ) 𝐵 ) )
16 2 1 10 13 nmval ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑁 ‘ 𝐴 ) = ( 𝐴 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) )
17 16 3ad2ant2 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) = ( 𝐴 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) )
18 2 1 10 13 nmval ⊢ ( 𝐵 ∈ 𝑋 → ( 𝑁 ‘ 𝐵 ) = ( 𝐵 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) )
19 18 3ad2ant3 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐵 ) = ( 𝐵 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) )
20 17 19 oveq12d ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) − ( 𝑁 ‘ 𝐵 ) ) = ( ( 𝐴 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) − ( 𝐵 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ) )
21 20 fveq2d ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( abs ‘ ( ( 𝑁 ‘ 𝐴 ) − ( 𝑁 ‘ 𝐵 ) ) ) = ( abs ‘ ( ( 𝐴 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) − ( 𝐵 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ) ) )
22 2 1 3 13 ngpds ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) )
23 22 eqcomd ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) = ( 𝐴 ( dist ‘ 𝐺 ) 𝐵 ) )
24 15 21 23 3brtr4d ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( abs ‘ ( ( 𝑁 ‘ 𝐴 ) − ( 𝑁 ‘ 𝐵 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) )