Proof of Theorem metnrmlem1
Step | Hyp | Ref
| Expression |
1 | | 1re 10039 |
. . . 4
⊢ 1 ∈
ℝ |
2 | 1 | rexri 10097 |
. . 3
⊢ 1 ∈
ℝ* |
3 | | metnrmlem.1 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
4 | 3 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → 𝐷 ∈ (∞Met‘𝑋)) |
5 | | metnrmlem.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐽)) |
6 | 5 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → 𝑆 ∈ (Clsd‘𝐽)) |
7 | | eqid 2622 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 |
8 | 7 | cldss 20833 |
. . . . . . . 8
⊢ (𝑆 ∈ (Clsd‘𝐽) → 𝑆 ⊆ ∪ 𝐽) |
9 | 6, 8 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → 𝑆 ⊆ ∪ 𝐽) |
10 | | metdscn.j |
. . . . . . . . 9
⊢ 𝐽 = (MetOpen‘𝐷) |
11 | 10 | mopnuni 22246 |
. . . . . . . 8
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) |
12 | 4, 11 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → 𝑋 = ∪ 𝐽) |
13 | 9, 12 | sseqtr4d 3642 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → 𝑆 ⊆ 𝑋) |
14 | | metdscn.f |
. . . . . . 7
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, <
)) |
15 | 14 | metdsf 22651 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐹:𝑋⟶(0[,]+∞)) |
16 | 4, 13, 15 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → 𝐹:𝑋⟶(0[,]+∞)) |
17 | | metnrmlem.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ (Clsd‘𝐽)) |
18 | 17 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → 𝑇 ∈ (Clsd‘𝐽)) |
19 | 7 | cldss 20833 |
. . . . . . . 8
⊢ (𝑇 ∈ (Clsd‘𝐽) → 𝑇 ⊆ ∪ 𝐽) |
20 | 18, 19 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → 𝑇 ⊆ ∪ 𝐽) |
21 | 20, 12 | sseqtr4d 3642 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → 𝑇 ⊆ 𝑋) |
22 | | simprr 796 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → 𝐵 ∈ 𝑇) |
23 | 21, 22 | sseldd 3604 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → 𝐵 ∈ 𝑋) |
24 | 16, 23 | ffvelrnd 6360 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → (𝐹‘𝐵) ∈ (0[,]+∞)) |
25 | | elxrge0 12281 |
. . . . 5
⊢ ((𝐹‘𝐵) ∈ (0[,]+∞) ↔ ((𝐹‘𝐵) ∈ ℝ* ∧ 0 ≤
(𝐹‘𝐵))) |
26 | 25 | simplbi 476 |
. . . 4
⊢ ((𝐹‘𝐵) ∈ (0[,]+∞) → (𝐹‘𝐵) ∈
ℝ*) |
27 | 24, 26 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → (𝐹‘𝐵) ∈
ℝ*) |
28 | | ifcl 4130 |
. . 3
⊢ ((1
∈ ℝ* ∧ (𝐹‘𝐵) ∈ ℝ*) → if(1
≤ (𝐹‘𝐵), 1, (𝐹‘𝐵)) ∈
ℝ*) |
29 | 2, 27, 28 | sylancr 695 |
. 2
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → if(1 ≤ (𝐹‘𝐵), 1, (𝐹‘𝐵)) ∈
ℝ*) |
30 | | simprl 794 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → 𝐴 ∈ 𝑆) |
31 | 13, 30 | sseldd 3604 |
. . 3
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → 𝐴 ∈ 𝑋) |
32 | | xmetcl 22136 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈
ℝ*) |
33 | 4, 31, 23, 32 | syl3anc 1326 |
. 2
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → (𝐴𝐷𝐵) ∈
ℝ*) |
34 | | xrmin2 12009 |
. . 3
⊢ ((1
∈ ℝ* ∧ (𝐹‘𝐵) ∈ ℝ*) → if(1
≤ (𝐹‘𝐵), 1, (𝐹‘𝐵)) ≤ (𝐹‘𝐵)) |
35 | 2, 27, 34 | sylancr 695 |
. 2
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → if(1 ≤ (𝐹‘𝐵), 1, (𝐹‘𝐵)) ≤ (𝐹‘𝐵)) |
36 | 14 | metdstri 22654 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐹‘𝐵) ≤ ((𝐵𝐷𝐴) +𝑒 (𝐹‘𝐴))) |
37 | 4, 13, 23, 31, 36 | syl22anc 1327 |
. . 3
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → (𝐹‘𝐵) ≤ ((𝐵𝐷𝐴) +𝑒 (𝐹‘𝐴))) |
38 | | xmetsym 22152 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐵𝐷𝐴) = (𝐴𝐷𝐵)) |
39 | 4, 23, 31, 38 | syl3anc 1326 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → (𝐵𝐷𝐴) = (𝐴𝐷𝐵)) |
40 | 14 | metds0 22653 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → (𝐹‘𝐴) = 0) |
41 | 4, 13, 30, 40 | syl3anc 1326 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → (𝐹‘𝐴) = 0) |
42 | 39, 41 | oveq12d 6668 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → ((𝐵𝐷𝐴) +𝑒 (𝐹‘𝐴)) = ((𝐴𝐷𝐵) +𝑒 0)) |
43 | | xaddid1 12072 |
. . . . 5
⊢ ((𝐴𝐷𝐵) ∈ ℝ* → ((𝐴𝐷𝐵) +𝑒 0) = (𝐴𝐷𝐵)) |
44 | 33, 43 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → ((𝐴𝐷𝐵) +𝑒 0) = (𝐴𝐷𝐵)) |
45 | 42, 44 | eqtrd 2656 |
. . 3
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → ((𝐵𝐷𝐴) +𝑒 (𝐹‘𝐴)) = (𝐴𝐷𝐵)) |
46 | 37, 45 | breqtrd 4679 |
. 2
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → (𝐹‘𝐵) ≤ (𝐴𝐷𝐵)) |
47 | 29, 27, 33, 35, 46 | xrletrd 11993 |
1
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → if(1 ≤ (𝐹‘𝐵), 1, (𝐹‘𝐵)) ≤ (𝐴𝐷𝐵)) |