Metamath Proof Explorer

Theorem norm3lem

Description: Lemma involving norm of differences in Hilbert space. (Contributed by NM, 18-Aug-1999) (New usage is discouraged.)

Ref Expression
Hypotheses norm3dif.1 ⊢ 𝐴 ∈ ℋ
norm3dif.2 ⊢ 𝐵 ∈ ℋ
norm3dif.3 ⊢ 𝐶 ∈ ℋ
norm3lem.4 ⊢ 𝐷 ∈ ℝ
Assertion norm3lem ( ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) < ( 𝐷 / 2 ) ) → ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) < 𝐷 )

Proof

Step Hyp Ref Expression
1 norm3dif.1 ⊢ 𝐴 ∈ ℋ
2 norm3dif.2 ⊢ 𝐵 ∈ ℋ
3 norm3dif.3 ⊢ 𝐶 ∈ ℋ
4 norm3lem.4 ⊢ 𝐷 ∈ ℝ
5 1 2 3 norm3difi ⊢ ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ≤ ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) + ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) )
6 1 3 hvsubcli ⊢ ( 𝐴 −ℎ 𝐶 ) ∈ ℋ
7 6 normcli ⊢ ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) ∈ ℝ
8 3 2 hvsubcli ⊢ ( 𝐶 −ℎ 𝐵 ) ∈ ℋ
9 8 normcli ⊢ ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) ∈ ℝ
10 4 rehalfcli ⊢ ( 𝐷 / 2 ) ∈ ℝ
11 7 9 10 10 lt2addi ⊢ ( ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) < ( 𝐷 / 2 ) ) → ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) + ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) ) < ( ( 𝐷 / 2 ) + ( 𝐷 / 2 ) ) )
12 1 2 hvsubcli ⊢ ( 𝐴 −ℎ 𝐵 ) ∈ ℋ
13 12 normcli ⊢ ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ∈ ℝ
14 7 9 readdcli ⊢ ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) + ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) ) ∈ ℝ
15 10 10 readdcli ⊢ ( ( 𝐷 / 2 ) + ( 𝐷 / 2 ) ) ∈ ℝ
16 13 14 15 lelttri ⊢ ( ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ≤ ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) + ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) ) ∧ ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) + ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) ) < ( ( 𝐷 / 2 ) + ( 𝐷 / 2 ) ) ) → ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) < ( ( 𝐷 / 2 ) + ( 𝐷 / 2 ) ) )
17 5 11 16 sylancr ⊢ ( ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) < ( 𝐷 / 2 ) ) → ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) < ( ( 𝐷 / 2 ) + ( 𝐷 / 2 ) ) )
18 10 recni ⊢ ( 𝐷 / 2 ) ∈ ℂ
19 18 2timesi ⊢ ( 2 · ( 𝐷 / 2 ) ) = ( ( 𝐷 / 2 ) + ( 𝐷 / 2 ) )
20 4 recni ⊢ 𝐷 ∈ ℂ
21 2cn ⊢ 2 ∈ ℂ
22 2ne0 ⊢ 2 ≠ 0
23 20 21 22 divcan2i ⊢ ( 2 · ( 𝐷 / 2 ) ) = 𝐷
24 19 23 eqtr3i ⊢ ( ( 𝐷 / 2 ) + ( 𝐷 / 2 ) ) = 𝐷
25 17 24 breqtrdi ⊢ ( ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) < ( 𝐷 / 2 ) ) → ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) < 𝐷 )