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=BaseG
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=BaseG
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 ⊢0G=0G
11 1 10 grpidcl ⊢G∈Grp→0G∈X
12 9 11 syl ⊢G∈NrmGrp∧A∈X∧B∈X→0G∈X
13 eqid ⊢dist⁡G=dist⁡G
14 1 13 msrtri ⊢G∈MetSp∧A∈X∧B∈X∧0G∈X→Adist⁡G0G−Bdist⁡G0G≤Adist⁡GB
15 5 6 7 12 14 syl13anc ⊢G∈NrmGrp∧A∈X∧B∈X→Adist⁡G0G−Bdist⁡G0G≤Adist⁡GB
16 2 1 10 13 nmval ⊢A∈X→N⁡A=Adist⁡G0G
17 16 3ad2ant2 ⊢G∈NrmGrp∧A∈X∧B∈X→N⁡A=Adist⁡G0G
18 2 1 10 13 nmval ⊢B∈X→N⁡B=Bdist⁡G0G
19 18 3ad2ant3 ⊢G∈NrmGrp∧A∈X∧B∈X→N⁡B=Bdist⁡G0G
20 17 19 oveq12d ⊢G∈NrmGrp∧A∈X∧B∈X→N⁡A−N⁡B=Adist⁡G0G−Bdist⁡G0G
21 20 fveq2d ⊢G∈NrmGrp∧A∈X∧B∈X→N⁡A−N⁡B=Adist⁡G0G−Bdist⁡G0G
22 2 1 3 13 ngpds ⊢G∈NrmGrp∧A∈X∧B∈X→Adist⁡GB=N⁡A-˙B
23 22 eqcomd ⊢G∈NrmGrp∧A∈X∧B∈X→N⁡A-˙B=Adist⁡GB
24 15 21 23 3brtr4d ⊢G∈NrmGrp∧A∈X∧B∈X→N⁡A−N⁡B≤N⁡A-˙B