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ℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) < 𝐷 )