Proof of Theorem metss2lem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | metss2.2 | . . . . . . 7
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) | 
| 2 | 1 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → 𝐷 ∈ (Met‘𝑋)) | 
| 3 |  | simplrl 776 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → 𝑥 ∈ 𝑋) | 
| 4 |  | simpr 484 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) | 
| 5 |  | metcl 24343 | . . . . . 6
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) ∈ ℝ) | 
| 6 | 2, 3, 4, 5 | syl3anc 1372 | . . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) ∈ ℝ) | 
| 7 |  | simplrr 777 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → 𝑆 ∈
ℝ+) | 
| 8 | 7 | rpred 13078 | . . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → 𝑆 ∈ ℝ) | 
| 9 |  | metss2.3 | . . . . . 6
⊢ (𝜑 → 𝑅 ∈
ℝ+) | 
| 10 | 9 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → 𝑅 ∈
ℝ+) | 
| 11 | 6, 8, 10 | ltmuldiv2d 13126 | . . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → ((𝑅 · (𝑥𝐷𝑦)) < 𝑆 ↔ (𝑥𝐷𝑦) < (𝑆 / 𝑅))) | 
| 12 |  | metss2.4 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦))) | 
| 13 | 12 | anassrs 467 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦))) | 
| 14 | 13 | adantlrr 721 | . . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦))) | 
| 15 |  | metss2.1 | . . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ (Met‘𝑋)) | 
| 16 | 15 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → 𝐶 ∈ (Met‘𝑋)) | 
| 17 |  | metcl 24343 | . . . . . . 7
⊢ ((𝐶 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐶𝑦) ∈ ℝ) | 
| 18 | 16, 3, 4, 17 | syl3anc 1372 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → (𝑥𝐶𝑦) ∈ ℝ) | 
| 19 | 10 | rpred 13078 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → 𝑅 ∈ ℝ) | 
| 20 | 19, 6 | remulcld 11292 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → (𝑅 · (𝑥𝐷𝑦)) ∈ ℝ) | 
| 21 |  | lelttr 11352 | . . . . . 6
⊢ (((𝑥𝐶𝑦) ∈ ℝ ∧ (𝑅 · (𝑥𝐷𝑦)) ∈ ℝ ∧ 𝑆 ∈ ℝ) → (((𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦)) ∧ (𝑅 · (𝑥𝐷𝑦)) < 𝑆) → (𝑥𝐶𝑦) < 𝑆)) | 
| 22 | 18, 20, 8, 21 | syl3anc 1372 | . . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → (((𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦)) ∧ (𝑅 · (𝑥𝐷𝑦)) < 𝑆) → (𝑥𝐶𝑦) < 𝑆)) | 
| 23 | 14, 22 | mpand 695 | . . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → ((𝑅 · (𝑥𝐷𝑦)) < 𝑆 → (𝑥𝐶𝑦) < 𝑆)) | 
| 24 | 11, 23 | sylbird 260 | . . 3
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐷𝑦) < (𝑆 / 𝑅) → (𝑥𝐶𝑦) < 𝑆)) | 
| 25 | 24 | ss2rabdv 4075 | . 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < (𝑆 / 𝑅)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝑥𝐶𝑦) < 𝑆}) | 
| 26 |  | metxmet 24345 | . . . . 5
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) | 
| 27 | 1, 26 | syl 17 | . . . 4
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) | 
| 28 | 27 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → 𝐷 ∈ (∞Met‘𝑋)) | 
| 29 |  | simprl 770 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → 𝑥 ∈ 𝑋) | 
| 30 |  | simpr 484 | . . . . 5
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+) → 𝑆 ∈
ℝ+) | 
| 31 |  | rpdivcl 13061 | . . . . 5
⊢ ((𝑆 ∈ ℝ+
∧ 𝑅 ∈
ℝ+) → (𝑆 / 𝑅) ∈
ℝ+) | 
| 32 | 30, 9, 31 | syl2anr 597 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → (𝑆 / 𝑅) ∈
ℝ+) | 
| 33 | 32 | rpxrd 13079 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → (𝑆 / 𝑅) ∈
ℝ*) | 
| 34 |  | blval 24397 | . . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ (𝑆 / 𝑅) ∈ ℝ*) → (𝑥(ball‘𝐷)(𝑆 / 𝑅)) = {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < (𝑆 / 𝑅)}) | 
| 35 | 28, 29, 33, 34 | syl3anc 1372 | . 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → (𝑥(ball‘𝐷)(𝑆 / 𝑅)) = {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < (𝑆 / 𝑅)}) | 
| 36 |  | metxmet 24345 | . . . . 5
⊢ (𝐶 ∈ (Met‘𝑋) → 𝐶 ∈ (∞Met‘𝑋)) | 
| 37 | 15, 36 | syl 17 | . . . 4
⊢ (𝜑 → 𝐶 ∈ (∞Met‘𝑋)) | 
| 38 | 37 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → 𝐶 ∈ (∞Met‘𝑋)) | 
| 39 |  | rpxr 13045 | . . . 4
⊢ (𝑆 ∈ ℝ+
→ 𝑆 ∈
ℝ*) | 
| 40 | 39 | ad2antll 729 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → 𝑆 ∈
ℝ*) | 
| 41 |  | blval 24397 | . . 3
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ*) → (𝑥(ball‘𝐶)𝑆) = {𝑦 ∈ 𝑋 ∣ (𝑥𝐶𝑦) < 𝑆}) | 
| 42 | 38, 29, 40, 41 | syl3anc 1372 | . 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → (𝑥(ball‘𝐶)𝑆) = {𝑦 ∈ 𝑋 ∣ (𝑥𝐶𝑦) < 𝑆}) | 
| 43 | 25, 35, 42 | 3sstr4d 4038 | 1
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → (𝑥(ball‘𝐷)(𝑆 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑆)) |