This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nm2dif

Description: Inequality for the difference of norms. (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypotheses nmf.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
nmf.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
nmmtri.m ⊢ − = ( -g ‘ 𝐺 )
Assertion nm2dif ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) − ( 𝑁 ‘ 𝐵 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 nmf.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 nmf.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
3 nmmtri.m ⊢ − = ( -g ‘ 𝐺 )
4 1 2 nmcl ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
5 4 3adant3 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
6 1 2 nmcl ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐵 ) ∈ ℝ )
7 6 3adant2 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐵 ) ∈ ℝ )
8 5 7 resubcld ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) − ( 𝑁 ‘ 𝐵 ) ) ∈ ℝ )
9 8 recnd ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) − ( 𝑁 ‘ 𝐵 ) ) ∈ ℂ )
10 9 abscld ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( abs ‘ ( ( 𝑁 ‘ 𝐴 ) − ( 𝑁 ‘ 𝐵 ) ) ) ∈ ℝ )
11 simp1 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐺 ∈ NrmGrp )
12 ngpgrp ⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ Grp )
13 1 3 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 − 𝐵 ) ∈ 𝑋 )
14 12 13 syl3an1 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 − 𝐵 ) ∈ 𝑋 )
15 1 2 nmcl ⊢ ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴 − 𝐵 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ )
16 11 14 15 syl2anc ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ )
17 8 leabsd ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) − ( 𝑁 ‘ 𝐵 ) ) ≤ ( abs ‘ ( ( 𝑁 ‘ 𝐴 ) − ( 𝑁 ‘ 𝐵 ) ) ) )
18 1 2 3 nmrtri ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( abs ‘ ( ( 𝑁 ‘ 𝐴 ) − ( 𝑁 ‘ 𝐵 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) )
19 8 10 16 17 18 letrd ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) − ( 𝑁 ‘ 𝐵 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) )