Metamath Proof Explorer

Theorem norm3dif

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

Ref Expression
Assertion norm3dif ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → norm ℎ ⁡ A - ℎ B ≤ norm ℎ ⁡ A - ℎ C + norm ℎ ⁡ C - ℎ B

Proof

Step Hyp Ref Expression
1 fvoveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B
2 fvoveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ C = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C
3 2 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ C + norm ℎ ⁡ C - ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C + norm ℎ ⁡ C - ℎ B
4 1 3 breq12d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ B ≤ norm ℎ ⁡ A - ℎ C + norm ℎ ⁡ C - ℎ B ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B ≤ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C + norm ℎ ⁡ C - ℎ B
5 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ B = if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
6 5 fveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
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 oveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C + norm ℎ ⁡ C - ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C + norm ℎ ⁡ C - ℎ if B ∈ ℋ B 0 ℎ
10 6 9 breq12d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B ≤ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C + norm ℎ ⁡ C - ℎ B ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ ≤ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C + norm ℎ ⁡ C - ℎ if B ∈ ℋ B 0 ℎ
11 oveq2 ⊢ C = if C ∈ ℋ C 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ C = if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ
12 11 fveq2d ⊢ C = if C ∈ ℋ C 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ
13 fvoveq1 ⊢ C = if C ∈ ℋ C 0 ℎ → norm ℎ ⁡ C - ℎ if B ∈ ℋ B 0 ℎ = norm ℎ ⁡ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
14 12 13 oveq12d ⊢ C = if C ∈ ℋ C 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C + norm ℎ ⁡ C - ℎ if B ∈ ℋ B 0 ℎ = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ + norm ℎ ⁡ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
15 14 breq2d ⊢ C = if C ∈ ℋ C 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ ≤ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C + norm ℎ ⁡ C - ℎ if B ∈ ℋ B 0 ℎ ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ ≤ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ + norm ℎ ⁡ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
16 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
17 ifhvhv0 ⊢ if B ∈ ℋ B 0 ℎ ∈ ℋ
18 ifhvhv0 ⊢ if C ∈ ℋ C 0 ℎ ∈ ℋ
19 16 17 18 norm3difi ⊢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ ≤ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ + norm ℎ ⁡ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
20 4 10 15 19 dedth3h ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → norm ℎ ⁡ A - ℎ B ≤ norm ℎ ⁡ A - ℎ C + norm ℎ ⁡ C - ℎ B