Proof of Theorem norm3dif
Step | Hyp | Ref
| Expression |
1 | | oveq1 6556 |
. . . 4
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐴 −ℎ
𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵)) |
2 | 1 | fveq2d 6107 |
. . 3
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(normℎ‘(𝐴 −ℎ 𝐵)) =
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))) |
3 | | oveq1 6556 |
. . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐴 −ℎ
𝐶) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐶)) |
4 | 3 | fveq2d 6107 |
. . . 4
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
(normℎ‘(𝐴 −ℎ 𝐶)) =
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐶))) |
5 | 4 | oveq1d 6564 |
. . 3
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
((normℎ‘(𝐴 −ℎ 𝐶)) +
(normℎ‘(𝐶 −ℎ 𝐵))) =
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐶)) + (normℎ‘(𝐶 −ℎ
𝐵)))) |
6 | 2, 5 | breq12d 4596 |
. 2
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) →
((normℎ‘(𝐴 −ℎ 𝐵)) ≤
((normℎ‘(𝐴 −ℎ 𝐶)) +
(normℎ‘(𝐶 −ℎ 𝐵))) ↔
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵)) ≤
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐶)) + (normℎ‘(𝐶 −ℎ
𝐵))))) |
7 | | oveq2 6557 |
. . . 4
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) |
8 | 7 | fveq2d 6107 |
. . 3
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵)) =
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) |
9 | | oveq2 6557 |
. . . . 5
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (𝐶 −ℎ
𝐵) = (𝐶 −ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ))) |
10 | 9 | fveq2d 6107 |
. . . 4
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
(normℎ‘(𝐶 −ℎ 𝐵)) =
(normℎ‘(𝐶 −ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))) |
11 | 10 | oveq2d 6565 |
. . 3
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐶)) + (normℎ‘(𝐶 −ℎ
𝐵))) =
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐶)) + (normℎ‘(𝐶 −ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ))))) |
12 | 8, 11 | breq12d 4596 |
. 2
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) →
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵)) ≤
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐶)) + (normℎ‘(𝐶 −ℎ
𝐵))) ↔
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) ≤
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐶)) + (normℎ‘(𝐶 −ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))))) |
13 | | oveq2 6557 |
. . . . 5
⊢ (𝐶 = if(𝐶 ∈ ℋ, 𝐶, 0ℎ) → (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐶) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐶 ∈ ℋ, 𝐶, 0ℎ))) |
14 | 13 | fveq2d 6107 |
. . . 4
⊢ (𝐶 = if(𝐶 ∈ ℋ, 𝐶, 0ℎ) →
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐶)) =
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐶 ∈ ℋ, 𝐶, 0ℎ)))) |
15 | | oveq1 6556 |
. . . . 5
⊢ (𝐶 = if(𝐶 ∈ ℋ, 𝐶, 0ℎ) → (𝐶 −ℎ
if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) =
(if(𝐶 ∈ ℋ, 𝐶, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) |
16 | 15 | fveq2d 6107 |
. . . 4
⊢ (𝐶 = if(𝐶 ∈ ℋ, 𝐶, 0ℎ) →
(normℎ‘(𝐶 −ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) =
(normℎ‘(if(𝐶 ∈ ℋ, 𝐶, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) |
17 | 14, 16 | oveq12d 6567 |
. . 3
⊢ (𝐶 = if(𝐶 ∈ ℋ, 𝐶, 0ℎ) →
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐶)) + (normℎ‘(𝐶 −ℎ
if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) =
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐶 ∈ ℋ, 𝐶, 0ℎ))) +
(normℎ‘(if(𝐶 ∈ ℋ, 𝐶, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))) |
18 | 17 | breq2d 4595 |
. 2
⊢ (𝐶 = if(𝐶 ∈ ℋ, 𝐶, 0ℎ) →
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) ≤
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐶)) + (normℎ‘(𝐶 −ℎ
if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))
↔ (normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) ≤
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐶 ∈ ℋ, 𝐶, 0ℎ))) +
(normℎ‘(if(𝐶 ∈ ℋ, 𝐶, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))))) |
19 | | ifhvhv0 27263 |
. . 3
⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈
ℋ |
20 | | ifhvhv0 27263 |
. . 3
⊢ if(𝐵 ∈ ℋ, 𝐵, 0ℎ) ∈
ℋ |
21 | | ifhvhv0 27263 |
. . 3
⊢ if(𝐶 ∈ ℋ, 𝐶, 0ℎ) ∈
ℋ |
22 | 19, 20, 21 | norm3difi 27388 |
. 2
⊢
(normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) ≤
((normℎ‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐶 ∈ ℋ, 𝐶, 0ℎ))) +
(normℎ‘(if(𝐶 ∈ ℋ, 𝐶, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) |
23 | 6, 12, 18, 22 | dedth3h 4091 |
1
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) →
(normℎ‘(𝐴 −ℎ 𝐵)) ≤
((normℎ‘(𝐴 −ℎ 𝐶)) +
(normℎ‘(𝐶 −ℎ 𝐵)))) |