Metamath Proof Explorer

Theorem norm3lemt

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

Ref Expression
Assertion norm3lemt ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℝ → norm ℎ ⁡ A - ℎ C < D 2 ∧ norm ℎ ⁡ C - ℎ B < D 2 → norm ℎ ⁡ A - ℎ B < D

Proof

Step Hyp Ref Expression
1 fvoveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ C = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C
2 1 breq1d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ C < D 2 ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C < D 2
3 2 anbi1d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ C < D 2 ∧ norm ℎ ⁡ C - ℎ B < D 2 ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C < D 2 ∧ norm ℎ ⁡ C - ℎ B < D 2
4 fvoveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B
5 4 breq1d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ B < D ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B < D
6 3 5 imbi12d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ C < D 2 ∧ norm ℎ ⁡ C - ℎ B < D 2 → norm ℎ ⁡ A - ℎ B < D ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C < D 2 ∧ norm ℎ ⁡ C - ℎ B < D 2 → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B < D
7 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → C - ℎ B = C - ℎ if B ∈ ℋ B 0 ℎ
8 7 fveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ C - ℎ B = norm ℎ ⁡ C - ℎ if B ∈ ℋ B 0 ℎ
9 8 breq1d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ C - ℎ B < D 2 ↔ norm ℎ ⁡ C - ℎ if B ∈ ℋ B 0 ℎ < D 2
10 9 anbi2d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C < D 2 ∧ norm ℎ ⁡ C - ℎ B < D 2 ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C < D 2 ∧ norm ℎ ⁡ C - ℎ if B ∈ ℋ B 0 ℎ < D 2
11 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ B = if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
12 11 fveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
13 12 breq1d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B < D ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ < D
14 10 13 imbi12d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C < D 2 ∧ norm ℎ ⁡ C - ℎ B < D 2 → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B < D ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C < D 2 ∧ norm ℎ ⁡ C - ℎ if B ∈ ℋ B 0 ℎ < D 2 → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ < D
15 oveq2 ⊢ C = if C ∈ ℋ C 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ C = if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ
16 15 fveq2d ⊢ C = if C ∈ ℋ C 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ
17 16 breq1d ⊢ C = if C ∈ ℋ C 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C < D 2 ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ < D 2
18 fvoveq1 ⊢ C = if C ∈ ℋ C 0 ℎ → norm ℎ ⁡ C - ℎ if B ∈ ℋ B 0 ℎ = norm ℎ ⁡ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
19 18 breq1d ⊢ C = if C ∈ ℋ C 0 ℎ → norm ℎ ⁡ C - ℎ if B ∈ ℋ B 0 ℎ < D 2 ↔ norm ℎ ⁡ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ < D 2
20 17 19 anbi12d ⊢ C = if C ∈ ℋ C 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C < D 2 ∧ norm ℎ ⁡ C - ℎ if B ∈ ℋ B 0 ℎ < D 2 ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ < D 2 ∧ norm ℎ ⁡ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ < D 2
21 20 imbi1d ⊢ C = if C ∈ ℋ C 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C < D 2 ∧ norm ℎ ⁡ C - ℎ if B ∈ ℋ B 0 ℎ < D 2 → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ < D ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ < D 2 ∧ norm ℎ ⁡ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ < D 2 → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ < D
22 oveq1 ⊢ D = if D ∈ ℝ D 2 → D 2 = if D ∈ ℝ D 2 2
23 22 breq2d ⊢ D = if D ∈ ℝ D 2 → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ < D 2 ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ < if D ∈ ℝ D 2 2
24 22 breq2d ⊢ D = if D ∈ ℝ D 2 → norm ℎ ⁡ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ < D 2 ↔ norm ℎ ⁡ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ < if D ∈ ℝ D 2 2
25 23 24 anbi12d ⊢ D = if D ∈ ℝ D 2 → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ < D 2 ∧ norm ℎ ⁡ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ < D 2 ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ < if D ∈ ℝ D 2 2 ∧ norm ℎ ⁡ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ < if D ∈ ℝ D 2 2
26 breq2 ⊢ D = if D ∈ ℝ D 2 → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ < D ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ < if D ∈ ℝ D 2
27 25 26 imbi12d ⊢ D = if D ∈ ℝ D 2 → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ < D 2 ∧ norm ℎ ⁡ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ < D 2 → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ < D ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ < if D ∈ ℝ D 2 2 ∧ norm ℎ ⁡ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ < if D ∈ ℝ D 2 2 → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ < if D ∈ ℝ D 2
28 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
29 ifhvhv0 ⊢ if B ∈ ℋ B 0 ℎ ∈ ℋ
30 ifhvhv0 ⊢ if C ∈ ℋ C 0 ℎ ∈ ℋ
31 2re ⊢ 2 ∈ ℝ
32 31 elimel ⊢ if D ∈ ℝ D 2 ∈ ℝ
33 28 29 30 32 norm3lem ⊢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ < if D ∈ ℝ D 2 2 ∧ norm ℎ ⁡ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ < if D ∈ ℝ D 2 2 → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ < if D ∈ ℝ D 2
34 6 14 21 27 33 dedth4h ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℝ → norm ℎ ⁡ A - ℎ C < D 2 ∧ norm ℎ ⁡ C - ℎ B < D 2 → norm ℎ ⁡ A - ℎ B < D