Step | Hyp | Ref
| Expression |
1 | | elin 3796 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ (𝐴 ∩ 𝐵) ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) |
2 | | cdj1.2 |
. . . . . . . . . . . . . 14
⊢ 𝐵 ∈
Sℋ |
3 | | neg1cn 11124 |
. . . . . . . . . . . . . 14
⊢ -1 ∈
ℂ |
4 | | shmulcl 28075 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈
Sℋ ∧ -1 ∈ ℂ ∧ 𝑤 ∈ 𝐵) → (-1
·ℎ 𝑤) ∈ 𝐵) |
5 | 2, 3, 4 | mp3an12 1414 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ 𝐵 → (-1
·ℎ 𝑤) ∈ 𝐵) |
6 | 5 | anim2i 593 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → (𝑤 ∈ 𝐴 ∧ (-1
·ℎ 𝑤) ∈ 𝐵)) |
7 | 1, 6 | sylbi 207 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ (𝐴 ∩ 𝐵) → (𝑤 ∈ 𝐴 ∧ (-1
·ℎ 𝑤) ∈ 𝐵)) |
8 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑤 → (normℎ‘𝑦) =
(normℎ‘𝑤)) |
9 | 8 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑤 → ((normℎ‘𝑦) +
(normℎ‘𝑧)) = ((normℎ‘𝑤) +
(normℎ‘𝑧))) |
10 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑤 → (𝑦 +ℎ 𝑧) = (𝑤 +ℎ 𝑧)) |
11 | 10 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑤 → (normℎ‘(𝑦 +ℎ 𝑧)) =
(normℎ‘(𝑤 +ℎ 𝑧))) |
12 | 11 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑤 → (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) = (𝑥 ·
(normℎ‘(𝑤 +ℎ 𝑧)))) |
13 | 9, 12 | breq12d 4666 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 →
(((normℎ‘𝑦) + (normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) ↔
((normℎ‘𝑤) + (normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ 𝑧))))) |
14 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (-1
·ℎ 𝑤) → (normℎ‘𝑧) =
(normℎ‘(-1 ·ℎ 𝑤))) |
15 | 14 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (-1
·ℎ 𝑤) →
((normℎ‘𝑤) + (normℎ‘𝑧)) =
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤)))) |
16 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (-1
·ℎ 𝑤) → (𝑤 +ℎ 𝑧) = (𝑤 +ℎ (-1
·ℎ 𝑤))) |
17 | 16 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (-1
·ℎ 𝑤) →
(normℎ‘(𝑤 +ℎ 𝑧)) = (normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))) |
18 | 17 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (-1
·ℎ 𝑤) → (𝑥 ·
(normℎ‘(𝑤 +ℎ 𝑧))) = (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤))))) |
19 | 15, 18 | breq12d 4666 |
. . . . . . . . . . . 12
⊢ (𝑧 = (-1
·ℎ 𝑤) →
(((normℎ‘𝑤) + (normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ 𝑧))) ↔
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))))) |
20 | 13, 19 | rspc2v 3322 |
. . . . . . . . . . 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 482 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ (𝐴 ∩ 𝐵)) → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) →
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))))) |
23 | | cdj1.1 |
. . . . . . . . . . . 12
⊢ 𝐴 ∈
Sℋ |
24 | 23, 2 | shincli 28221 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ 𝐵) ∈
Sℋ |
25 | 24 | sheli 28071 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (𝐴 ∩ 𝐵) → 𝑤 ∈ ℋ) |
26 | | normneg 28001 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℋ →
(normℎ‘(-1 ·ℎ 𝑤)) =
(normℎ‘𝑤)) |
27 | 26 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℋ →
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) = ((normℎ‘𝑤) +
(normℎ‘𝑤))) |
28 | | normcl 27982 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ℋ →
(normℎ‘𝑤) ∈ ℝ) |
29 | 28 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℋ →
(normℎ‘𝑤) ∈ ℂ) |
30 | 29 | 2timesd 11275 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℋ → (2
· (normℎ‘𝑤)) = ((normℎ‘𝑤) +
(normℎ‘𝑤))) |
31 | 27, 30 | eqtr4d 2659 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ℋ →
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) = (2 ·
(normℎ‘𝑤))) |
32 | 31 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ) →
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) = (2 ·
(normℎ‘𝑤))) |
33 | | hvnegid 27884 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℋ → (𝑤 +ℎ (-1
·ℎ 𝑤)) = 0ℎ) |
34 | 33 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ℋ →
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤))) =
(normℎ‘0ℎ)) |
35 | | norm0 27985 |
. . . . . . . . . . . . . . . 16
⊢
(normℎ‘0ℎ) =
0 |
36 | 34, 35 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℋ →
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤))) = 0) |
37 | 36 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℋ → (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))) = (𝑥 · 0)) |
38 | | recn 10026 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
39 | 38 | mul01d 10235 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ → (𝑥 · 0) =
0) |
40 | 37, 39 | sylan9eqr 2678 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ) → (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))) = 0) |
41 | | 2t0e0 11183 |
. . . . . . . . . . . . 13
⊢ (2
· 0) = 0 |
42 | 40, 41 | syl6eqr 2674 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ) → (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))) = (2 · 0)) |
43 | 32, 42 | breq12d 4666 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ) →
(((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))) ↔ (2 ·
(normℎ‘𝑤)) ≤ (2 · 0))) |
44 | | 0re 10040 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
45 | | letri3 10123 |
. . . . . . . . . . . . . . 15
⊢
(((normℎ‘𝑤) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((normℎ‘𝑤) = 0 ↔
((normℎ‘𝑤) ≤ 0 ∧ 0 ≤
(normℎ‘𝑤)))) |
46 | 28, 44, 45 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℋ →
((normℎ‘𝑤) = 0 ↔
((normℎ‘𝑤) ≤ 0 ∧ 0 ≤
(normℎ‘𝑤)))) |
47 | | normge0 27983 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℋ → 0 ≤
(normℎ‘𝑤)) |
48 | 47 | biantrud 528 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℋ →
((normℎ‘𝑤) ≤ 0 ↔
((normℎ‘𝑤) ≤ 0 ∧ 0 ≤
(normℎ‘𝑤)))) |
49 | | 2re 11090 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ |
50 | | 2pos 11112 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
2 |
51 | 49, 50 | pm3.2i 471 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℝ ∧ 0 < 2) |
52 | | lemul2 10876 |
. . . . . . . . . . . . . . . 16
⊢
(((normℎ‘𝑤) ∈ ℝ ∧ 0 ∈ ℝ ∧
(2 ∈ ℝ ∧ 0 < 2)) → ((normℎ‘𝑤) ≤ 0 ↔ (2 ·
(normℎ‘𝑤)) ≤ (2 · 0))) |
53 | 44, 51, 52 | mp3an23 1416 |
. . . . . . . . . . . . . . 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 297 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ℋ → ((2
· (normℎ‘𝑤)) ≤ (2 · 0) ↔
(normℎ‘𝑤) = 0)) |
56 | | norm-i 27986 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ℋ →
((normℎ‘𝑤) = 0 ↔ 𝑤 = 0ℎ)) |
57 | 55, 56 | bitrd 268 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ℋ → ((2
· (normℎ‘𝑤)) ≤ (2 · 0) ↔ 𝑤 =
0ℎ)) |
58 | 57 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ) → ((2
· (normℎ‘𝑤)) ≤ (2 · 0) ↔ 𝑤 =
0ℎ)) |
59 | 43, 58 | bitrd 268 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ) →
(((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))) ↔ 𝑤 = 0ℎ)) |
60 | 25, 59 | sylan2 491 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ (𝐴 ∩ 𝐵)) →
(((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))) ↔ 𝑤 = 0ℎ)) |
61 | 22, 60 | sylibd 229 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ (𝐴 ∩ 𝐵)) → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) → 𝑤 = 0ℎ)) |
62 | 61 | impancom 456 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧)))) → (𝑤 ∈ (𝐴 ∩ 𝐵) → 𝑤 = 0ℎ)) |
63 | | elch0 28111 |
. . . . . . 7
⊢ (𝑤 ∈ 0ℋ
↔ 𝑤 =
0ℎ) |
64 | 62, 63 | syl6ibr 242 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧)))) → (𝑤 ∈ (𝐴 ∩ 𝐵) → 𝑤 ∈
0ℋ)) |
65 | 64 | ssrdv 3609 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧)))) → (𝐴 ∩ 𝐵) ⊆
0ℋ) |
66 | 65 | ex 450 |
. . . 4
⊢ (𝑥 ∈ ℝ →
(∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) → (𝐴 ∩ 𝐵) ⊆
0ℋ)) |
67 | | shle0 28301 |
. . . . 5
⊢ ((𝐴 ∩ 𝐵) ∈ Sℋ
→ ((𝐴 ∩ 𝐵) ⊆ 0ℋ
↔ (𝐴 ∩ 𝐵) =
0ℋ)) |
68 | 24, 67 | ax-mp 5 |
. . . 4
⊢ ((𝐴 ∩ 𝐵) ⊆ 0ℋ ↔ (𝐴 ∩ 𝐵) = 0ℋ) |
69 | 66, 68 | syl6ib 241 |
. . 3
⊢ (𝑥 ∈ ℝ →
(∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) → (𝐴 ∩ 𝐵) = 0ℋ)) |
70 | 69 | adantld 483 |
. 2
⊢ (𝑥 ∈ ℝ → ((0 <
𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧)))) → (𝐴 ∩ 𝐵) = 0ℋ)) |
71 | 70 | rexlimiv 3027 |
1
⊢
(∃𝑥 ∈
ℝ (0 < 𝑥 ∧
∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧)))) → (𝐴 ∩ 𝐵) = 0ℋ) |