| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elin 3966 | . . . . . . . . . . . 12
⊢ (𝑤 ∈ (𝐴 ∩ 𝐵) ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) | 
| 2 |  | cdj1.2 | . . . . . . . . . . . . . 14
⊢ 𝐵 ∈
Sℋ | 
| 3 |  | neg1cn 12381 | . . . . . . . . . . . . . 14
⊢ -1 ∈
ℂ | 
| 4 |  | shmulcl 31238 | . . . . . . . . . . . . . 14
⊢ ((𝐵 ∈
Sℋ ∧ -1 ∈ ℂ ∧ 𝑤 ∈ 𝐵) → (-1
·ℎ 𝑤) ∈ 𝐵) | 
| 5 | 2, 3, 4 | mp3an12 1452 | . . . . . . . . . . . . 13
⊢ (𝑤 ∈ 𝐵 → (-1
·ℎ 𝑤) ∈ 𝐵) | 
| 6 | 5 | anim2i 617 | . . . . . . . . . . . 12
⊢ ((𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → (𝑤 ∈ 𝐴 ∧ (-1
·ℎ 𝑤) ∈ 𝐵)) | 
| 7 | 1, 6 | sylbi 217 | . . . . . . . . . . 11
⊢ (𝑤 ∈ (𝐴 ∩ 𝐵) → (𝑤 ∈ 𝐴 ∧ (-1
·ℎ 𝑤) ∈ 𝐵)) | 
| 8 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑤 → (normℎ‘𝑦) =
(normℎ‘𝑤)) | 
| 9 | 8 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝑤 → ((normℎ‘𝑦) +
(normℎ‘𝑧)) = ((normℎ‘𝑤) +
(normℎ‘𝑧))) | 
| 10 |  | fvoveq1 7455 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑤 → (normℎ‘(𝑦 +ℎ 𝑧)) =
(normℎ‘(𝑤 +ℎ 𝑧))) | 
| 11 | 10 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝑤 → (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) = (𝑥 ·
(normℎ‘(𝑤 +ℎ 𝑧)))) | 
| 12 | 9, 11 | breq12d 5155 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 →
(((normℎ‘𝑦) + (normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) ↔
((normℎ‘𝑤) + (normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ 𝑧))))) | 
| 13 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑧 = (-1
·ℎ 𝑤) → (normℎ‘𝑧) =
(normℎ‘(-1 ·ℎ 𝑤))) | 
| 14 | 13 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑧 = (-1
·ℎ 𝑤) →
((normℎ‘𝑤) + (normℎ‘𝑧)) =
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤)))) | 
| 15 |  | oveq2 7440 | . . . . . . . . . . . . . . 15
⊢ (𝑧 = (-1
·ℎ 𝑤) → (𝑤 +ℎ 𝑧) = (𝑤 +ℎ (-1
·ℎ 𝑤))) | 
| 16 | 15 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ (𝑧 = (-1
·ℎ 𝑤) →
(normℎ‘(𝑤 +ℎ 𝑧)) = (normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))) | 
| 17 | 16 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑧 = (-1
·ℎ 𝑤) → (𝑥 ·
(normℎ‘(𝑤 +ℎ 𝑧))) = (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤))))) | 
| 18 | 14, 17 | breq12d 5155 | . . . . . . . . . . . 12
⊢ (𝑧 = (-1
·ℎ 𝑤) →
(((normℎ‘𝑤) + (normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ 𝑧))) ↔
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))))) | 
| 19 | 12, 18 | rspc2v 3632 | . . . . . . . . . . 11
⊢ ((𝑤 ∈ 𝐴 ∧ (-1
·ℎ 𝑤) ∈ 𝐵) → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) →
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))))) | 
| 20 | 7, 19 | syl 17 | . . . . . . . . . 10
⊢ (𝑤 ∈ (𝐴 ∩ 𝐵) → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) →
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))))) | 
| 21 | 20 | adantl 481 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ (𝐴 ∩ 𝐵)) → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) →
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))))) | 
| 22 |  | cdj1.1 | . . . . . . . . . . . 12
⊢ 𝐴 ∈
Sℋ | 
| 23 | 22, 2 | shincli 31382 | . . . . . . . . . . 11
⊢ (𝐴 ∩ 𝐵) ∈
Sℋ | 
| 24 | 23 | sheli 31234 | . . . . . . . . . 10
⊢ (𝑤 ∈ (𝐴 ∩ 𝐵) → 𝑤 ∈ ℋ) | 
| 25 |  | normneg 31164 | . . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℋ →
(normℎ‘(-1 ·ℎ 𝑤)) =
(normℎ‘𝑤)) | 
| 26 | 25 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℋ →
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) = ((normℎ‘𝑤) +
(normℎ‘𝑤))) | 
| 27 |  | normcl 31145 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ℋ →
(normℎ‘𝑤) ∈ ℝ) | 
| 28 | 27 | recnd 11290 | . . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℋ →
(normℎ‘𝑤) ∈ ℂ) | 
| 29 | 28 | 2timesd 12511 | . . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℋ → (2
· (normℎ‘𝑤)) = ((normℎ‘𝑤) +
(normℎ‘𝑤))) | 
| 30 | 26, 29 | eqtr4d 2779 | . . . . . . . . . . . . 13
⊢ (𝑤 ∈ ℋ →
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) = (2 ·
(normℎ‘𝑤))) | 
| 31 | 30 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ) →
((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) = (2 ·
(normℎ‘𝑤))) | 
| 32 |  | hvnegid 31047 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℋ → (𝑤 +ℎ (-1
·ℎ 𝑤)) = 0ℎ) | 
| 33 | 32 | fveq2d 6909 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ℋ →
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤))) =
(normℎ‘0ℎ)) | 
| 34 |  | norm0 31148 | . . . . . . . . . . . . . . . 16
⊢
(normℎ‘0ℎ) =
0 | 
| 35 | 33, 34 | eqtrdi 2792 | . . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℋ →
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤))) = 0) | 
| 36 | 35 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℋ → (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))) = (𝑥 · 0)) | 
| 37 |  | recn 11246 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) | 
| 38 | 37 | mul01d 11461 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ → (𝑥 · 0) =
0) | 
| 39 | 36, 38 | sylan9eqr 2798 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ) → (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))) = 0) | 
| 40 |  | 2t0e0 12436 | . . . . . . . . . . . . 13
⊢ (2
· 0) = 0 | 
| 41 | 39, 40 | eqtr4di 2794 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ) → (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))) = (2 · 0)) | 
| 42 | 31, 41 | breq12d 5155 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ) →
(((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))) ↔ (2 ·
(normℎ‘𝑤)) ≤ (2 · 0))) | 
| 43 |  | 0re 11264 | . . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ | 
| 44 |  | letri3 11347 | . . . . . . . . . . . . . . 15
⊢
(((normℎ‘𝑤) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((normℎ‘𝑤) = 0 ↔
((normℎ‘𝑤) ≤ 0 ∧ 0 ≤
(normℎ‘𝑤)))) | 
| 45 | 27, 43, 44 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℋ →
((normℎ‘𝑤) = 0 ↔
((normℎ‘𝑤) ≤ 0 ∧ 0 ≤
(normℎ‘𝑤)))) | 
| 46 |  | normge0 31146 | . . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℋ → 0 ≤
(normℎ‘𝑤)) | 
| 47 | 46 | biantrud 531 | . . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℋ →
((normℎ‘𝑤) ≤ 0 ↔
((normℎ‘𝑤) ≤ 0 ∧ 0 ≤
(normℎ‘𝑤)))) | 
| 48 |  | 2re 12341 | . . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ | 
| 49 |  | 2pos 12370 | . . . . . . . . . . . . . . . . 17
⊢ 0 <
2 | 
| 50 | 48, 49 | pm3.2i 470 | . . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℝ ∧ 0 < 2) | 
| 51 |  | lemul2 12121 | . . . . . . . . . . . . . . . 16
⊢
(((normℎ‘𝑤) ∈ ℝ ∧ 0 ∈ ℝ ∧
(2 ∈ ℝ ∧ 0 < 2)) → ((normℎ‘𝑤) ≤ 0 ↔ (2 ·
(normℎ‘𝑤)) ≤ (2 · 0))) | 
| 52 | 43, 50, 51 | mp3an23 1454 | . . . . . . . . . . . . . . 15
⊢
((normℎ‘𝑤) ∈ ℝ →
((normℎ‘𝑤) ≤ 0 ↔ (2 ·
(normℎ‘𝑤)) ≤ (2 · 0))) | 
| 53 | 27, 52 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℋ →
((normℎ‘𝑤) ≤ 0 ↔ (2 ·
(normℎ‘𝑤)) ≤ (2 · 0))) | 
| 54 | 45, 47, 53 | 3bitr2rd 308 | . . . . . . . . . . . . 13
⊢ (𝑤 ∈ ℋ → ((2
· (normℎ‘𝑤)) ≤ (2 · 0) ↔
(normℎ‘𝑤) = 0)) | 
| 55 |  | norm-i 31149 | . . . . . . . . . . . . 13
⊢ (𝑤 ∈ ℋ →
((normℎ‘𝑤) = 0 ↔ 𝑤 = 0ℎ)) | 
| 56 | 54, 55 | bitrd 279 | . . . . . . . . . . . 12
⊢ (𝑤 ∈ ℋ → ((2
· (normℎ‘𝑤)) ≤ (2 · 0) ↔ 𝑤 =
0ℎ)) | 
| 57 | 56 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ) → ((2
· (normℎ‘𝑤)) ≤ (2 · 0) ↔ 𝑤 =
0ℎ)) | 
| 58 | 42, 57 | bitrd 279 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ ℋ) →
(((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))) ↔ 𝑤 = 0ℎ)) | 
| 59 | 24, 58 | sylan2 593 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ (𝐴 ∩ 𝐵)) →
(((normℎ‘𝑤) + (normℎ‘(-1
·ℎ 𝑤))) ≤ (𝑥 ·
(normℎ‘(𝑤 +ℎ (-1
·ℎ 𝑤)))) ↔ 𝑤 = 0ℎ)) | 
| 60 | 21, 59 | sylibd 239 | . . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑤 ∈ (𝐴 ∩ 𝐵)) → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) → 𝑤 = 0ℎ)) | 
| 61 | 60 | impancom 451 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧)))) → (𝑤 ∈ (𝐴 ∩ 𝐵) → 𝑤 = 0ℎ)) | 
| 62 |  | elch0 31274 | . . . . . . 7
⊢ (𝑤 ∈ 0ℋ
↔ 𝑤 =
0ℎ) | 
| 63 | 61, 62 | imbitrrdi 252 | . . . . . 6
⊢ ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧)))) → (𝑤 ∈ (𝐴 ∩ 𝐵) → 𝑤 ∈
0ℋ)) | 
| 64 | 63 | ssrdv 3988 | . . . . 5
⊢ ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧)))) → (𝐴 ∩ 𝐵) ⊆
0ℋ) | 
| 65 | 64 | ex 412 | . . . 4
⊢ (𝑥 ∈ ℝ →
(∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) → (𝐴 ∩ 𝐵) ⊆
0ℋ)) | 
| 66 |  | shle0 31462 | . . . . 5
⊢ ((𝐴 ∩ 𝐵) ∈ Sℋ
→ ((𝐴 ∩ 𝐵) ⊆ 0ℋ
↔ (𝐴 ∩ 𝐵) =
0ℋ)) | 
| 67 | 23, 66 | ax-mp 5 | . . . 4
⊢ ((𝐴 ∩ 𝐵) ⊆ 0ℋ ↔ (𝐴 ∩ 𝐵) = 0ℋ) | 
| 68 | 65, 67 | imbitrdi 251 | . . 3
⊢ (𝑥 ∈ ℝ →
(∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧))) → (𝐴 ∩ 𝐵) = 0ℋ)) | 
| 69 | 68 | adantld 490 | . 2
⊢ (𝑥 ∈ ℝ → ((0 <
𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧)))) → (𝐴 ∩ 𝐵) = 0ℋ)) | 
| 70 | 69 | rexlimiv 3147 | 1
⊢
(∃𝑥 ∈
ℝ (0 < 𝑥 ∧
∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) +
(normℎ‘𝑧)) ≤ (𝑥 ·
(normℎ‘(𝑦 +ℎ 𝑧)))) → (𝐴 ∩ 𝐵) = 0ℋ) |