Step | Hyp | Ref
| Expression |
1 | | simp1 1135 |
. . . . 5
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐶 ∈ (∞Met‘𝑋)) |
2 | | xmetcl 23484 |
. . . . . . 7
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐶𝑦) ∈
ℝ*) |
3 | | xmetge0 23497 |
. . . . . . 7
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝑥𝐶𝑦)) |
4 | | elxrge0 13189 |
. . . . . . 7
⊢ ((𝑥𝐶𝑦) ∈ (0[,]+∞) ↔ ((𝑥𝐶𝑦) ∈ ℝ* ∧ 0 ≤
(𝑥𝐶𝑦))) |
5 | 2, 3, 4 | sylanbrc 583 |
. . . . . 6
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐶𝑦) ∈ (0[,]+∞)) |
6 | 5 | 3expb 1119 |
. . . . 5
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ∈ (0[,]+∞)) |
7 | 1, 6 | sylan 580 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ∈ (0[,]+∞)) |
8 | | xmetf 23482 |
. . . . . . 7
⊢ (𝐶 ∈ (∞Met‘𝑋) → 𝐶:(𝑋 × 𝑋)⟶ℝ*) |
9 | 8 | 3ad2ant1 1132 |
. . . . . 6
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐶:(𝑋 × 𝑋)⟶ℝ*) |
10 | 9 | ffnd 6601 |
. . . . 5
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐶 Fn (𝑋 × 𝑋)) |
11 | | fnov 7405 |
. . . . 5
⊢ (𝐶 Fn (𝑋 × 𝑋) ↔ 𝐶 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝐶𝑦))) |
12 | 10, 11 | sylib 217 |
. . . 4
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐶 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝐶𝑦))) |
13 | | eqidd 2739 |
. . . 4
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → (𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) = (𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))) |
14 | | breq1 5077 |
. . . . 5
⊢ (𝑧 = (𝑥𝐶𝑦) → (𝑧 ≤ 𝑅 ↔ (𝑥𝐶𝑦) ≤ 𝑅)) |
15 | | id 22 |
. . . . 5
⊢ (𝑧 = (𝑥𝐶𝑦) → 𝑧 = (𝑥𝐶𝑦)) |
16 | 14, 15 | ifbieq1d 4483 |
. . . 4
⊢ (𝑧 = (𝑥𝐶𝑦) → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) = if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅)) |
17 | 7, 12, 13, 16 | fmpoco 7935 |
. . 3
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → ((𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) ∘ 𝐶) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅))) |
18 | | stdbdmet.1 |
. . 3
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅)) |
19 | 17, 18 | eqtr4di 2796 |
. 2
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → ((𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) ∘ 𝐶) = 𝐷) |
20 | | eliccxr 13167 |
. . . . 5
⊢ (𝑧 ∈ (0[,]+∞) →
𝑧 ∈
ℝ*) |
21 | | simp2 1136 |
. . . . 5
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝑅 ∈
ℝ*) |
22 | | ifcl 4504 |
. . . . 5
⊢ ((𝑧 ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) ∈
ℝ*) |
23 | 20, 21, 22 | syl2anr 597 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑧 ∈ (0[,]+∞)) → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) ∈
ℝ*) |
24 | 23 | fmpttd 6989 |
. . 3
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → (𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅)):(0[,]+∞)⟶ℝ*) |
25 | | id 22 |
. . . . . 6
⊢ (𝑎 ∈ (0[,]+∞) →
𝑎 ∈
(0[,]+∞)) |
26 | | vex 3436 |
. . . . . . 7
⊢ 𝑎 ∈ V |
27 | | ifexg 4508 |
. . . . . . 7
⊢ ((𝑎 ∈ V ∧ 𝑅 ∈ ℝ*)
→ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈ V) |
28 | 26, 21, 27 | sylancr 587 |
. . . . . 6
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈ V) |
29 | | breq1 5077 |
. . . . . . . 8
⊢ (𝑧 = 𝑎 → (𝑧 ≤ 𝑅 ↔ 𝑎 ≤ 𝑅)) |
30 | | id 22 |
. . . . . . . 8
⊢ (𝑧 = 𝑎 → 𝑧 = 𝑎) |
31 | 29, 30 | ifbieq1d 4483 |
. . . . . . 7
⊢ (𝑧 = 𝑎 → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) = if(𝑎 ≤ 𝑅, 𝑎, 𝑅)) |
32 | | eqid 2738 |
. . . . . . 7
⊢ (𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) = (𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) |
33 | 31, 32 | fvmptg 6873 |
. . . . . 6
⊢ ((𝑎 ∈ (0[,]+∞) ∧
if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈ V) → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) = if(𝑎 ≤ 𝑅, 𝑎, 𝑅)) |
34 | 25, 28, 33 | syl2anr 597 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → ((𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) = if(𝑎 ≤ 𝑅, 𝑎, 𝑅)) |
35 | 34 | eqeq1d 2740 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → (((𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) = 0 ↔ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0)) |
36 | | eqeq1 2742 |
. . . . . 6
⊢ (𝑎 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (𝑎 = 0 ↔ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0)) |
37 | 36 | bibi1d 344 |
. . . . 5
⊢ (𝑎 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → ((𝑎 = 0 ↔ 𝑎 = 0) ↔ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0 ↔ 𝑎 = 0))) |
38 | | eqeq1 2742 |
. . . . . 6
⊢ (𝑅 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (𝑅 = 0 ↔ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0)) |
39 | 38 | bibi1d 344 |
. . . . 5
⊢ (𝑅 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → ((𝑅 = 0 ↔ 𝑎 = 0) ↔ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0 ↔ 𝑎 = 0))) |
40 | | biidd 261 |
. . . . 5
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) ∧ 𝑎 ≤ 𝑅) → (𝑎 = 0 ↔ 𝑎 = 0)) |
41 | | simp3 1137 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 0 < 𝑅) |
42 | 41 | gt0ne0d 11539 |
. . . . . . . 8
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝑅 ≠ 0) |
43 | 42 | neneqd 2948 |
. . . . . . 7
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → ¬ 𝑅 = 0) |
44 | 43 | ad2antrr 723 |
. . . . . 6
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) ∧ ¬ 𝑎 ≤ 𝑅) → ¬ 𝑅 = 0) |
45 | | 0xr 11022 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
46 | | xrltle 12883 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ 𝑅 ∈ ℝ*) → (0 <
𝑅 → 0 ≤ 𝑅)) |
47 | 45, 21, 46 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → (0 < 𝑅 → 0 ≤ 𝑅)) |
48 | 41, 47 | mpd 15 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 0 ≤ 𝑅) |
49 | 48 | adantr 481 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → 0 ≤ 𝑅) |
50 | | breq1 5077 |
. . . . . . . 8
⊢ (𝑎 = 0 → (𝑎 ≤ 𝑅 ↔ 0 ≤ 𝑅)) |
51 | 49, 50 | syl5ibrcom 246 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → (𝑎 = 0 → 𝑎 ≤ 𝑅)) |
52 | 51 | con3dimp 409 |
. . . . . 6
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) ∧ ¬ 𝑎 ≤ 𝑅) → ¬ 𝑎 = 0) |
53 | 44, 52 | 2falsed 377 |
. . . . 5
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) ∧ ¬ 𝑎 ≤ 𝑅) → (𝑅 = 0 ↔ 𝑎 = 0)) |
54 | 37, 39, 40, 53 | ifbothda 4497 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0 ↔ 𝑎 = 0)) |
55 | 35, 54 | bitrd 278 |
. . 3
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → (((𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) = 0 ↔ 𝑎 = 0)) |
56 | | eliccxr 13167 |
. . . . . . . . 9
⊢ (𝑎 ∈ (0[,]+∞) →
𝑎 ∈
ℝ*) |
57 | 56 | ad2antrl 725 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 𝑎 ∈
ℝ*) |
58 | 21 | adantr 481 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 𝑅 ∈
ℝ*) |
59 | | xrmin1 12911 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑎) |
60 | 57, 58, 59 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑎) |
61 | 57, 58 | ifcld 4505 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈
ℝ*) |
62 | | eliccxr 13167 |
. . . . . . . . 9
⊢ (𝑏 ∈ (0[,]+∞) →
𝑏 ∈
ℝ*) |
63 | 62 | ad2antll 726 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 𝑏 ∈
ℝ*) |
64 | | xrletr 12892 |
. . . . . . . 8
⊢
((if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈ ℝ* ∧ 𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → ((if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑎 ∧ 𝑎 ≤ 𝑏) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏)) |
65 | 61, 57, 63, 64 | syl3anc 1370 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ ((if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑎 ∧ 𝑎 ≤ 𝑏) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏)) |
66 | 60, 65 | mpand 692 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑎 ≤ 𝑏 → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏)) |
67 | | xrmin2 12912 |
. . . . . . 7
⊢ ((𝑎 ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑅) |
68 | 57, 58, 67 | syl2anc 584 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑅) |
69 | 66, 68 | jctird 527 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑎 ≤ 𝑏 → (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏 ∧ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑅))) |
70 | | xrlemin 12918 |
. . . . . 6
⊢
((if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈ ℝ* ∧ 𝑏 ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ↔ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏 ∧ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑅))) |
71 | 61, 63, 58, 70 | syl3anc 1370 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ↔ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏 ∧ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑅))) |
72 | 69, 71 | sylibrd 258 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑎 ≤ 𝑏 → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
73 | 34 | adantrr 714 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ ((𝑧 ∈
(0[,]+∞) ↦ if(𝑧
≤ 𝑅, 𝑧, 𝑅))‘𝑎) = if(𝑎 ≤ 𝑅, 𝑎, 𝑅)) |
74 | | simpr 485 |
. . . . . 6
⊢ ((𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞))
→ 𝑏 ∈
(0[,]+∞)) |
75 | | vex 3436 |
. . . . . . 7
⊢ 𝑏 ∈ V |
76 | | ifexg 4508 |
. . . . . . 7
⊢ ((𝑏 ∈ V ∧ 𝑅 ∈ ℝ*)
→ if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ∈ V) |
77 | 75, 21, 76 | sylancr 587 |
. . . . . 6
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ∈ V) |
78 | | breq1 5077 |
. . . . . . . 8
⊢ (𝑧 = 𝑏 → (𝑧 ≤ 𝑅 ↔ 𝑏 ≤ 𝑅)) |
79 | | id 22 |
. . . . . . . 8
⊢ (𝑧 = 𝑏 → 𝑧 = 𝑏) |
80 | 78, 79 | ifbieq1d 4483 |
. . . . . . 7
⊢ (𝑧 = 𝑏 → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) = if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) |
81 | 80, 32 | fvmptg 6873 |
. . . . . 6
⊢ ((𝑏 ∈ (0[,]+∞) ∧
if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ∈ V) → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑏) = if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) |
82 | 74, 77, 81 | syl2anr 597 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ ((𝑧 ∈
(0[,]+∞) ↦ if(𝑧
≤ 𝑅, 𝑧, 𝑅))‘𝑏) = if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) |
83 | 73, 82 | breq12d 5087 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (((𝑧 ∈
(0[,]+∞) ↦ if(𝑧
≤ 𝑅, 𝑧, 𝑅))‘𝑎) ≤ ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑏) ↔ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
84 | 72, 83 | sylibrd 258 |
. . 3
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑎 ≤ 𝑏 → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) ≤ ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑏))) |
85 | 57, 63 | xaddcld 13035 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑎
+𝑒 𝑏)
∈ ℝ*) |
86 | | xrmin1 12911 |
. . . . . . 7
⊢ (((𝑎 +𝑒 𝑏) ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑏)) |
87 | 85, 58, 86 | syl2anc 584 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑏)) |
88 | 85, 58 | ifcld 4505 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ∈
ℝ*) |
89 | 57, 58 | xaddcld 13035 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑎
+𝑒 𝑅)
∈ ℝ*) |
90 | | xrmin2 12912 |
. . . . . . . 8
⊢ (((𝑎 +𝑒 𝑏) ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ 𝑅) |
91 | 85, 58, 90 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ 𝑅) |
92 | | xaddid2 12976 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ*
→ (0 +𝑒 𝑅) = 𝑅) |
93 | 58, 92 | syl 17 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (0 +𝑒 𝑅) = 𝑅) |
94 | 45 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 0 ∈ ℝ*) |
95 | | elxrge0 13189 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (0[,]+∞) ↔
(𝑎 ∈
ℝ* ∧ 0 ≤ 𝑎)) |
96 | 95 | simprbi 497 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (0[,]+∞) → 0
≤ 𝑎) |
97 | 96 | ad2antrl 725 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 0 ≤ 𝑎) |
98 | | xleadd1a 12987 |
. . . . . . . . 9
⊢ (((0
∈ ℝ* ∧ 𝑎 ∈ ℝ* ∧ 𝑅 ∈ ℝ*)
∧ 0 ≤ 𝑎) → (0
+𝑒 𝑅)
≤ (𝑎
+𝑒 𝑅)) |
99 | 94, 57, 58, 97, 98 | syl31anc 1372 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (0 +𝑒 𝑅) ≤ (𝑎 +𝑒 𝑅)) |
100 | 93, 99 | eqbrtrrd 5098 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 𝑅 ≤ (𝑎 +𝑒 𝑅)) |
101 | 88, 58, 89, 91, 100 | xrletrd 12896 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑅)) |
102 | | oveq2 7283 |
. . . . . . . 8
⊢ (𝑏 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (𝑎 +𝑒 𝑏) = (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
103 | 102 | breq2d 5086 |
. . . . . . 7
⊢ (𝑏 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑏) ↔ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))) |
104 | | oveq2 7283 |
. . . . . . . 8
⊢ (𝑅 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (𝑎 +𝑒 𝑅) = (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
105 | 104 | breq2d 5086 |
. . . . . . 7
⊢ (𝑅 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑅) ↔ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))) |
106 | 103, 105 | ifboth 4498 |
. . . . . 6
⊢
((if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑏) ∧ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑅)) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
107 | 87, 101, 106 | syl2anc 584 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
108 | 63, 58 | ifcld 4505 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ∈
ℝ*) |
109 | 58, 108 | xaddcld 13035 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑅
+𝑒 if(𝑏
≤ 𝑅, 𝑏, 𝑅)) ∈
ℝ*) |
110 | 58 | xaddid1d 12977 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑅
+𝑒 0) = 𝑅) |
111 | | elxrge0 13189 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (0[,]+∞) ↔
(𝑏 ∈
ℝ* ∧ 0 ≤ 𝑏)) |
112 | 111 | simprbi 497 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (0[,]+∞) → 0
≤ 𝑏) |
113 | 112 | ad2antll 726 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 0 ≤ 𝑏) |
114 | 48 | adantr 481 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 0 ≤ 𝑅) |
115 | | breq2 5078 |
. . . . . . . . . 10
⊢ (𝑏 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (0 ≤ 𝑏 ↔ 0 ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
116 | | breq2 5078 |
. . . . . . . . . 10
⊢ (𝑅 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (0 ≤ 𝑅 ↔ 0 ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
117 | 115, 116 | ifboth 4498 |
. . . . . . . . 9
⊢ ((0 ≤
𝑏 ∧ 0 ≤ 𝑅) → 0 ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) |
118 | 113, 114,
117 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 0 ≤ if(𝑏 ≤
𝑅, 𝑏, 𝑅)) |
119 | | xleadd2a 12988 |
. . . . . . . 8
⊢ (((0
∈ ℝ* ∧ if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ∈ ℝ* ∧ 𝑅 ∈ ℝ*)
∧ 0 ≤ if(𝑏 ≤
𝑅, 𝑏, 𝑅)) → (𝑅 +𝑒 0) ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
120 | 94, 108, 58, 118, 119 | syl31anc 1372 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑅
+𝑒 0) ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
121 | 110, 120 | eqbrtrrd 5098 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 𝑅 ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
122 | 88, 58, 109, 91, 121 | xrletrd 12896 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
123 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑎 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) = (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
124 | 123 | breq2d 5086 |
. . . . . 6
⊢ (𝑎 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) ↔ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))) |
125 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑅 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) = (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
126 | 125 | breq2d 5086 |
. . . . . 6
⊢ (𝑅 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) ↔ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))) |
127 | 124, 126 | ifboth 4498 |
. . . . 5
⊢
((if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) ∧ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
128 | 107, 122,
127 | syl2anc 584 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
129 | | ge0xaddcl 13194 |
. . . . 5
⊢ ((𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞))
→ (𝑎
+𝑒 𝑏)
∈ (0[,]+∞)) |
130 | | ovex 7308 |
. . . . . 6
⊢ (𝑎 +𝑒 𝑏) ∈ V |
131 | | ifexg 4508 |
. . . . . 6
⊢ (((𝑎 +𝑒 𝑏) ∈ V ∧ 𝑅 ∈ ℝ*)
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ∈ V) |
132 | 130, 21, 131 | sylancr 587 |
. . . . 5
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ∈ V) |
133 | | breq1 5077 |
. . . . . . 7
⊢ (𝑧 = (𝑎 +𝑒 𝑏) → (𝑧 ≤ 𝑅 ↔ (𝑎 +𝑒 𝑏) ≤ 𝑅)) |
134 | | id 22 |
. . . . . . 7
⊢ (𝑧 = (𝑎 +𝑒 𝑏) → 𝑧 = (𝑎 +𝑒 𝑏)) |
135 | 133, 134 | ifbieq1d 4483 |
. . . . . 6
⊢ (𝑧 = (𝑎 +𝑒 𝑏) → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) = if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅)) |
136 | 135, 32 | fvmptg 6873 |
. . . . 5
⊢ (((𝑎 +𝑒 𝑏) ∈ (0[,]+∞) ∧
if((𝑎 +𝑒
𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ∈ V) → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘(𝑎 +𝑒 𝑏)) = if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅)) |
137 | 129, 132,
136 | syl2anr 597 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ ((𝑧 ∈
(0[,]+∞) ↦ if(𝑧
≤ 𝑅, 𝑧, 𝑅))‘(𝑎 +𝑒 𝑏)) = if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅)) |
138 | 73, 82 | oveq12d 7293 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (((𝑧 ∈
(0[,]+∞) ↦ if(𝑧
≤ 𝑅, 𝑧, 𝑅))‘𝑎) +𝑒 ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑏)) = (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
139 | 128, 137,
138 | 3brtr4d 5106 |
. . 3
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ ((𝑧 ∈
(0[,]+∞) ↦ if(𝑧
≤ 𝑅, 𝑧, 𝑅))‘(𝑎 +𝑒 𝑏)) ≤ (((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) +𝑒 ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑏))) |
140 | 1, 24, 55, 84, 139 | comet 23669 |
. 2
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → ((𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) ∘ 𝐶) ∈ (∞Met‘𝑋)) |
141 | 19, 140 | eqeltrrd 2840 |
1
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐷 ∈ (∞Met‘𝑋)) |