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

Metamath Proof Explorer

Theorem norm3adifii

Description: Norm of differences around common element. Part of Lemma 3.6 of Beran p. 101. (Contributed by NM, 30-Sep-1999) (New usage is discouraged.)

Ref Expression
Hypotheses norm3dif.1 ⊢ 𝐴 ∈ ℋ
norm3dif.2 ⊢ 𝐵 ∈ ℋ
norm3dif.3 ⊢ 𝐶 ∈ ℋ
Assertion norm3adifii ( abs ‘ ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) − ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 norm3dif.1 ⊢ 𝐴 ∈ ℋ
2 norm3dif.2 ⊢ 𝐵 ∈ ℋ
3 norm3dif.3 ⊢ 𝐶 ∈ ℋ
4 1 3 hvsubcli ⊢ ( 𝐴 −ℎ 𝐶 ) ∈ ℋ
5 4 normcli ⊢ ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) ∈ ℝ
6 5 recni ⊢ ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) ∈ ℂ
7 2 3 hvsubcli ⊢ ( 𝐵 −ℎ 𝐶 ) ∈ ℋ
8 7 normcli ⊢ ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) ∈ ℝ
9 8 recni ⊢ ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) ∈ ℂ
10 6 9 negsubdi2i ⊢ - ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) − ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) ) = ( ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) − ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) )
11 2 3 1 norm3difi ⊢ ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) ≤ ( ( normℎ ‘ ( 𝐵 −ℎ 𝐴 ) ) + ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) )
12 2 1 normsubi ⊢ ( normℎ ‘ ( 𝐵 −ℎ 𝐴 ) ) = ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) )
13 12 oveq1i ⊢ ( ( normℎ ‘ ( 𝐵 −ℎ 𝐴 ) ) + ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) ) = ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) + ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) )
14 11 13 breqtri ⊢ ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) ≤ ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) + ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) )
15 1 2 hvsubcli ⊢ ( 𝐴 −ℎ 𝐵 ) ∈ ℋ
16 15 normcli ⊢ ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ∈ ℝ
17 8 5 16 lesubaddi ⊢ ( ( ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) − ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↔ ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) ≤ ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) + ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) ) )
18 14 17 mpbir ⊢ ( ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) − ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) )
19 10 18 eqbrtri ⊢ - ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) − ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) )
20 5 8 resubcli ⊢ ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) − ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) ) ∈ ℝ
21 20 16 lenegcon1i ⊢ ( - ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) − ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↔ - ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ≤ ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) − ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) ) )
22 19 21 mpbi ⊢ - ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ≤ ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) − ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) )
23 1 3 2 norm3difi ⊢ ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) ≤ ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) + ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) )
24 5 8 16 lesubaddi ⊢ ( ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) − ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↔ ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) ≤ ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) + ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) ) )
25 23 24 mpbir ⊢ ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) − ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) )
26 20 16 abslei ⊢ ( ( abs ‘ ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) − ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↔ ( - ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ≤ ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) − ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) ) ∧ ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) − ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ) )
27 22 25 26 mpbir2an ⊢ ( abs ‘ ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) − ( normℎ ‘ ( 𝐵 −ℎ 𝐶 ) ) ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) )