Step | Hyp | Ref
| Expression |
1 | | elin 3758 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ (𝐴 ∩ 𝐵) ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) |
2 | | cdj1.2 |
. . . . . . . . . . . . . 14
⊢ 𝐵 ∈
Sℋ |
3 | | neg1cn 11001 |
. . . . . . . . . . . . . 14
⊢ -1 ∈
ℂ |
4 | | shmulcl 27459 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈
Sℋ ∧ -1 ∈ ℂ ∧ 𝑤 ∈ 𝐵) → (-1
·ℎ 𝑤) ∈ 𝐵) |
5 | 2, 3, 4 | mp3an12 1406 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ 𝐵 → (-1
·ℎ 𝑤) ∈ 𝐵) |
6 | 5 | anim2i 591 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → (𝑤 ∈ 𝐴 ∧ (-1
·ℎ 𝑤) ∈ 𝐵)) |
7 | 1, 6 | sylbi 206 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ (𝐴 ∩ 𝐵) → (𝑤 ∈ 𝐴 ∧ (-1
·ℎ 𝑤) ∈ 𝐵)) |
8 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑤 → (normℎ‘𝑦) =
(normℎ‘𝑤)) |
9 | 8 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑤 → ((normℎ‘𝑦) +
(normℎ‘𝑧)) = ((normℎ‘𝑤) +
(normℎ‘𝑧))) |
10 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑤 → (𝑦 +ℎ 𝑧) = (𝑤 +ℎ 𝑧)) |
11 | 10 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑤 → (normℎ‘(𝑦 +ℎ 𝑧)) =
(normℎ‘(𝑤 +ℎ 𝑧))) |
12 | 11 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑤 → (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) = (𝑥 ·
(normℎ‘(𝑤 +ℎ 𝑧)))) |
13 | 9, 12 | breq12d 4596 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 →
(((normℎ‘𝑦) + (normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) ↔
((normℎ‘𝑤) + (normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ 𝑧))))) |
14 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (-1
·ℎ 𝑤) → (normℎ‘𝑧) =
(normℎ‘(-1 ·ℎ 𝑤))) |
15 | 14 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (-1
·ℎ 𝑤) →
((normℎ‘𝑤) + (normℎ‘𝑧)) =
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤)))) |
16 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (-1
·ℎ 𝑤) → (𝑤 +ℎ 𝑧) = (𝑤 +ℎ (-1
·ℎ 𝑤))) |
17 | 16 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (-1
·ℎ 𝑤) →
(normℎ‘(𝑤 +ℎ 𝑧)) = (normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))) |
18 | 17 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (-1
·ℎ 𝑤) → (𝑥 ·
(normℎ‘(𝑤 +ℎ 𝑧))) = (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤))))) |
19 | 15, 18 | breq12d 4596 |
. . . . . . . . . . . 12
⊢ (𝑧 = (-1
·ℎ 𝑤) →
(((normℎ‘𝑤) + (normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ 𝑧))) ↔
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))))) |
20 | 13, 19 | rspc2v 3293 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ 𝐴 ∧ (-1
·ℎ 𝑤) ∈ 𝐵) → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) →
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))))) |
21 | 7, 20 | syl 17 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (𝐴 ∩ 𝐵) → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) →
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))))) |
22 | 21 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ (𝐴 ∩ 𝐵)) → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) →
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))))) |
23 | | cdj1.1 |
. . . . . . . . . . . 12
⊢ 𝐴 ∈
Sℋ |
24 | 23, 2 | shincli 27605 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ 𝐵) ∈
Sℋ |
25 | 24 | sheli 27455 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (𝐴 ∩ 𝐵) → 𝑤 ∈ ℋ) |
26 | | normneg 27385 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℋ →
(normℎ‘(-1 ·ℎ 𝑤)) =
(normℎ‘𝑤)) |
27 | 26 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℋ →
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) = ((normℎ‘𝑤) +
(normℎ‘𝑤))) |
28 | | normcl 27366 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ℋ →
(normℎ‘𝑤) ∈ ℝ) |
29 | 28 | recnd 9947 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℋ →
(normℎ‘𝑤) ∈ ℂ) |
30 | 29 | 2timesd 11152 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℋ → (2
· (normℎ‘𝑤)) = ((normℎ‘𝑤) +
(normℎ‘𝑤))) |
31 | 27, 30 | eqtr4d 2647 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ℋ →
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) = (2 ·
(normℎ‘𝑤))) |
32 | 31 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ) →
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) = (2 ·
(normℎ‘𝑤))) |
33 | | hvnegid 27268 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℋ → (𝑤 +ℎ (-1
·ℎ 𝑤)) = 0ℎ) |
34 | 33 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ℋ →
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤))) =
(normℎ‘0ℎ)) |
35 | | norm0 27369 |
. . . . . . . . . . . . . . . 16
⊢
(normℎ‘0ℎ) =
0 |
36 | 34, 35 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℋ →
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤))) = 0) |
37 | 36 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℋ → (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))) = (𝑥 · 0)) |
38 | | recn 9905 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
39 | 38 | mul01d 10114 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ → (𝑥 · 0) =
0) |
40 | 37, 39 | sylan9eqr 2666 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ) → (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))) = 0) |
41 | | 2t0e0 11060 |
. . . . . . . . . . . . 13
⊢ (2
· 0) = 0 |
42 | 40, 41 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ) → (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))) = (2 · 0)) |
43 | 32, 42 | breq12d 4596 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ) →
(((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))) ↔ (2 ·
(normℎ‘𝑤)) ≤ (2 · 0))) |
44 | | 0re 9919 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
45 | | letri3 10002 |
. . . . . . . . . . . . . . 15
⊢
(((normℎ‘𝑤) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((normℎ‘𝑤) = 0 ↔
((normℎ‘𝑤) ≤ 0 ∧ 0 ≤
(normℎ‘𝑤)))) |
46 | 28, 44, 45 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℋ →
((normℎ‘𝑤) = 0 ↔
((normℎ‘𝑤) ≤ 0 ∧ 0 ≤
(normℎ‘𝑤)))) |
47 | | normge0 27367 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℋ → 0 ≤
(normℎ‘𝑤)) |
48 | 47 | biantrud 527 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℋ →
((normℎ‘𝑤) ≤ 0 ↔
((normℎ‘𝑤) ≤ 0 ∧ 0 ≤
(normℎ‘𝑤)))) |
49 | | 2re 10967 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ |
50 | | 2pos 10989 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
2 |
51 | 49, 50 | pm3.2i 470 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℝ ∧ 0 < 2) |
52 | | lemul2 10755 |
. . . . . . . . . . . . . . . 16
⊢
(((normℎ‘𝑤) ∈ ℝ ∧ 0 ∈ ℝ ∧
(2 ∈ ℝ ∧ 0 < 2)) → ((normℎ‘𝑤) ≤ 0 ↔ (2 ·
(normℎ‘𝑤)) ≤ (2 · 0))) |
53 | 44, 51, 52 | mp3an23 1408 |
. . . . . . . . . . . . . . 15
⊢
((normℎ‘𝑤) ∈ ℝ →
((normℎ‘𝑤) ≤ 0 ↔ (2 ·
(normℎ‘𝑤)) ≤ (2 · 0))) |
54 | 28, 53 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℋ →
((normℎ‘𝑤) ≤ 0 ↔ (2 ·
(normℎ‘𝑤)) ≤ (2 · 0))) |
55 | 46, 48, 54 | 3bitr2rd 296 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ℋ → ((2
· (normℎ‘𝑤)) ≤ (2 · 0) ↔
(normℎ‘𝑤) = 0)) |
56 | | norm-i 27370 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ℋ →
((normℎ‘𝑤) = 0 ↔ 𝑤 = 0ℎ)) |
57 | 55, 56 | bitrd 267 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ℋ → ((2
· (normℎ‘𝑤)) ≤ (2 · 0) ↔ 𝑤 =
0ℎ)) |
58 | 57 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ) → ((2
· (normℎ‘𝑤)) ≤ (2 · 0) ↔ 𝑤 =
0ℎ)) |
59 | 43, 58 | bitrd 267 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ) →
(((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))) ↔ 𝑤 = 0ℎ)) |
60 | 25, 59 | sylan2 490 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ (𝐴 ∩ 𝐵)) →
(((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))) ↔ 𝑤 = 0ℎ)) |
61 | 22, 60 | sylibd 228 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ (𝐴 ∩ 𝐵)) → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) → 𝑤 = 0ℎ)) |
62 | 61 | impancom 455 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧)))) → (𝑤 ∈ (𝐴 ∩ 𝐵) → 𝑤 = 0ℎ)) |
63 | | elch0 27495 |
. . . . . . 7
⊢ (𝑤 ∈ 0ℋ
↔ 𝑤 =
0ℎ) |
64 | 62, 63 | syl6ibr 241 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧)))) → (𝑤 ∈ (𝐴 ∩ 𝐵) → 𝑤 ∈
0ℋ)) |
65 | 64 | ssrdv 3574 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧)))) → (𝐴 ∩ 𝐵) ⊆
0ℋ) |
66 | 65 | ex 449 |
. . . 4
⊢ (𝑥 ∈ ℝ →
(∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) → (𝐴 ∩ 𝐵) ⊆
0ℋ)) |
67 | | shle0 27685 |
. . . . 5
⊢ ((𝐴 ∩ 𝐵) ∈ Sℋ
→ ((𝐴 ∩ 𝐵) ⊆ 0ℋ
↔ (𝐴 ∩ 𝐵) =
0ℋ)) |
68 | 24, 67 | ax-mp 5 |
. . . 4
⊢ ((𝐴 ∩ 𝐵) ⊆ 0ℋ ↔ (𝐴 ∩ 𝐵) = 0ℋ) |
69 | 66, 68 | syl6ib 240 |
. . 3
⊢ (𝑥 ∈ ℝ →
(∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) → (𝐴 ∩ 𝐵) = 0ℋ)) |
70 | 69 | adantld 482 |
. 2
⊢ (𝑥 ∈ ℝ → ((0 <
𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧)))) → (𝐴 ∩ 𝐵) = 0ℋ)) |
71 | 70 | rexlimiv 3009 |
1
⊢
(∃𝑥 ∈
ℝ (0 < 𝑥 ∧
∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧)))) → (𝐴 ∩ 𝐵) = 0ℋ) |