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

Metamath Proof Explorer

Theorem norm3adifi

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

Ref Expression
Hypothesis norm3adift.1 ⊢ C ∈ ℋ
Assertion norm3adifi ⊢ A ∈ ℋ ∧ B ∈ ℋ → norm ℎ ⁡ A - ℎ C − norm ℎ ⁡ B - ℎ C ≤ norm ℎ ⁡ A - ℎ B

Proof

Step Hyp Ref Expression
1 norm3adift.1 ⊢ C ∈ ℋ
2 fvoveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ C = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C
3 2 fvoveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ C − norm ℎ ⁡ B - ℎ C = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C − norm ℎ ⁡ B - ℎ C
4 fvoveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B
5 3 4 breq12d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A - ℎ C − norm ℎ ⁡ B - ℎ C ≤ norm ℎ ⁡ A - ℎ B ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C − norm ℎ ⁡ B - ℎ C ≤ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B
6 fvoveq1 ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ B - ℎ C = norm ℎ ⁡ if B ∈ ℋ B 0 ℎ - ℎ C
7 6 oveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C − norm ℎ ⁡ B - ℎ C = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C − norm ℎ ⁡ if B ∈ ℋ B 0 ℎ - ℎ C
8 7 fveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C − norm ℎ ⁡ B - ℎ C = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C − norm ℎ ⁡ if B ∈ ℋ B 0 ℎ - ℎ C
9 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ B = if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
10 9 fveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
11 8 10 breq12d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C − norm ℎ ⁡ B - ℎ C ≤ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ B ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C − norm ℎ ⁡ if B ∈ ℋ B 0 ℎ - ℎ C ≤ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
12 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
13 ifhvhv0 ⊢ if B ∈ ℋ B 0 ℎ ∈ ℋ
14 12 13 1 norm3adifii ⊢ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ C − norm ℎ ⁡ if B ∈ ℋ B 0 ℎ - ℎ C ≤ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
15 5 11 14 dedth2h ⊢ A ∈ ℋ ∧ B ∈ ℋ → norm ℎ ⁡ A - ℎ C − norm ℎ ⁡ B - ℎ C ≤ norm ℎ ⁡ A - ℎ B