Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . . . 5
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐶 ∈ (∞Met‘𝑋)) |
2 | | xmetcl 23077 |
. . . . . . 7
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐶𝑦) ∈
ℝ*) |
3 | | xmetge0 23090 |
. . . . . . 7
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝑥𝐶𝑦)) |
4 | | elxrge0 12924 |
. . . . . . 7
⊢ ((𝑥𝐶𝑦) ∈ (0[,]+∞) ↔ ((𝑥𝐶𝑦) ∈ ℝ* ∧ 0 ≤
(𝑥𝐶𝑦))) |
5 | 2, 3, 4 | sylanbrc 586 |
. . . . . 6
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐶𝑦) ∈ (0[,]+∞)) |
6 | 5 | 3expb 1121 |
. . . . 5
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ∈ (0[,]+∞)) |
7 | 1, 6 | sylan 583 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ∈ (0[,]+∞)) |
8 | | xmetf 23075 |
. . . . . . 7
⊢ (𝐶 ∈ (∞Met‘𝑋) → 𝐶:(𝑋 × 𝑋)⟶ℝ*) |
9 | 8 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐶:(𝑋 × 𝑋)⟶ℝ*) |
10 | 9 | ffnd 6499 |
. . . . 5
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐶 Fn (𝑋 × 𝑋)) |
11 | | fnov 7291 |
. . . . 5
⊢ (𝐶 Fn (𝑋 × 𝑋) ↔ 𝐶 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝐶𝑦))) |
12 | 10, 11 | sylib 221 |
. . . 4
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐶 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝐶𝑦))) |
13 | | eqidd 2739 |
. . . 4
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → (𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) = (𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))) |
14 | | breq1 5030 |
. . . . 5
⊢ (𝑧 = (𝑥𝐶𝑦) → (𝑧 ≤ 𝑅 ↔ (𝑥𝐶𝑦) ≤ 𝑅)) |
15 | | id 22 |
. . . . 5
⊢ (𝑧 = (𝑥𝐶𝑦) → 𝑧 = (𝑥𝐶𝑦)) |
16 | 14, 15 | ifbieq1d 4435 |
. . . 4
⊢ (𝑧 = (𝑥𝐶𝑦) → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) = if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅)) |
17 | 7, 12, 13, 16 | fmpoco 7809 |
. . 3
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → ((𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) ∘ 𝐶) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅))) |
18 | | stdbdmet.1 |
. . 3
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅)) |
19 | 17, 18 | eqtr4di 2791 |
. 2
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → ((𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) ∘ 𝐶) = 𝐷) |
20 | | eliccxr 12902 |
. . . . 5
⊢ (𝑧 ∈ (0[,]+∞) →
𝑧 ∈
ℝ*) |
21 | | simp2 1138 |
. . . . 5
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝑅 ∈
ℝ*) |
22 | | ifcl 4456 |
. . . . 5
⊢ ((𝑧 ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) ∈
ℝ*) |
23 | 20, 21, 22 | syl2anr 600 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑧 ∈ (0[,]+∞)) → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) ∈
ℝ*) |
24 | 23 | fmpttd 6883 |
. . 3
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → (𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅)):(0[,]+∞)⟶ℝ*) |
25 | | id 22 |
. . . . . 6
⊢ (𝑎 ∈ (0[,]+∞) →
𝑎 ∈
(0[,]+∞)) |
26 | | vex 3401 |
. . . . . . 7
⊢ 𝑎 ∈ V |
27 | | ifexg 4460 |
. . . . . . 7
⊢ ((𝑎 ∈ V ∧ 𝑅 ∈ ℝ*)
→ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈ V) |
28 | 26, 21, 27 | sylancr 590 |
. . . . . 6
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈ V) |
29 | | breq1 5030 |
. . . . . . . 8
⊢ (𝑧 = 𝑎 → (𝑧 ≤ 𝑅 ↔ 𝑎 ≤ 𝑅)) |
30 | | id 22 |
. . . . . . . 8
⊢ (𝑧 = 𝑎 → 𝑧 = 𝑎) |
31 | 29, 30 | ifbieq1d 4435 |
. . . . . . 7
⊢ (𝑧 = 𝑎 → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) = if(𝑎 ≤ 𝑅, 𝑎, 𝑅)) |
32 | | eqid 2738 |
. . . . . . 7
⊢ (𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) = (𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) |
33 | 31, 32 | fvmptg 6767 |
. . . . . 6
⊢ ((𝑎 ∈ (0[,]+∞) ∧
if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈ V) → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) = if(𝑎 ≤ 𝑅, 𝑎, 𝑅)) |
34 | 25, 28, 33 | syl2anr 600 |
. . . . 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 347 |
. . . . 5
⊢ (𝑎 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → ((𝑎 = 0 ↔ 𝑎 = 0) ↔ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0 ↔ 𝑎 = 0))) |
38 | | eqeq1 2742 |
. . . . . 6
⊢ (𝑅 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (𝑅 = 0 ↔ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0)) |
39 | 38 | bibi1d 347 |
. . . . 5
⊢ (𝑅 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → ((𝑅 = 0 ↔ 𝑎 = 0) ↔ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0 ↔ 𝑎 = 0))) |
40 | | biidd 265 |
. . . . 5
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) ∧ 𝑎 ≤ 𝑅) → (𝑎 = 0 ↔ 𝑎 = 0)) |
41 | | simp3 1139 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 0 < 𝑅) |
42 | 41 | gt0ne0d 11275 |
. . . . . . . 8
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝑅 ≠ 0) |
43 | 42 | neneqd 2939 |
. . . . . . 7
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → ¬ 𝑅 = 0) |
44 | 43 | ad2antrr 726 |
. . . . . 6
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) ∧ ¬ 𝑎 ≤ 𝑅) → ¬ 𝑅 = 0) |
45 | | 0xr 10759 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
46 | | xrltle 12618 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ 𝑅 ∈ ℝ*) → (0 <
𝑅 → 0 ≤ 𝑅)) |
47 | 45, 21, 46 | sylancr 590 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → (0 < 𝑅 → 0 ≤ 𝑅)) |
48 | 41, 47 | mpd 15 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 0 ≤ 𝑅) |
49 | 48 | adantr 484 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → 0 ≤ 𝑅) |
50 | | breq1 5030 |
. . . . . . . 8
⊢ (𝑎 = 0 → (𝑎 ≤ 𝑅 ↔ 0 ≤ 𝑅)) |
51 | 49, 50 | syl5ibrcom 250 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → (𝑎 = 0 → 𝑎 ≤ 𝑅)) |
52 | 51 | con3dimp 412 |
. . . . . 6
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) ∧ ¬ 𝑎 ≤ 𝑅) → ¬ 𝑎 = 0) |
53 | 44, 52 | 2falsed 380 |
. . . . 5
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) ∧ ¬ 𝑎 ≤ 𝑅) → (𝑅 = 0 ↔ 𝑎 = 0)) |
54 | 37, 39, 40, 53 | ifbothda 4449 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0 ↔ 𝑎 = 0)) |
55 | 35, 54 | bitrd 282 |
. . 3
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → (((𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) = 0 ↔ 𝑎 = 0)) |
56 | | eliccxr 12902 |
. . . . . . . . 9
⊢ (𝑎 ∈ (0[,]+∞) →
𝑎 ∈
ℝ*) |
57 | 56 | ad2antrl 728 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 𝑎 ∈
ℝ*) |
58 | 21 | adantr 484 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 𝑅 ∈
ℝ*) |
59 | | xrmin1 12646 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑎) |
60 | 57, 58, 59 | syl2anc 587 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑎) |
61 | 57, 58 | ifcld 4457 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈
ℝ*) |
62 | | eliccxr 12902 |
. . . . . . . . 9
⊢ (𝑏 ∈ (0[,]+∞) →
𝑏 ∈
ℝ*) |
63 | 62 | ad2antll 729 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 𝑏 ∈
ℝ*) |
64 | | xrletr 12627 |
. . . . . . . 8
⊢
((if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈ ℝ* ∧ 𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → ((if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑎 ∧ 𝑎 ≤ 𝑏) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏)) |
65 | 61, 57, 63, 64 | syl3anc 1372 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ ((if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑎 ∧ 𝑎 ≤ 𝑏) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏)) |
66 | 60, 65 | mpand 695 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑎 ≤ 𝑏 → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏)) |
67 | | xrmin2 12647 |
. . . . . . 7
⊢ ((𝑎 ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑅) |
68 | 57, 58, 67 | syl2anc 587 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑅) |
69 | 66, 68 | jctird 530 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑎 ≤ 𝑏 → (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏 ∧ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑅))) |
70 | | xrlemin 12653 |
. . . . . 6
⊢
((if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈ ℝ* ∧ 𝑏 ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ↔ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏 ∧ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑅))) |
71 | 61, 63, 58, 70 | syl3anc 1372 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ↔ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏 ∧ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑅))) |
72 | 69, 71 | sylibrd 262 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑎 ≤ 𝑏 → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
73 | 34 | adantrr 717 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ ((𝑧 ∈
(0[,]+∞) ↦ if(𝑧
≤ 𝑅, 𝑧, 𝑅))‘𝑎) = if(𝑎 ≤ 𝑅, 𝑎, 𝑅)) |
74 | | simpr 488 |
. . . . . 6
⊢ ((𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞))
→ 𝑏 ∈
(0[,]+∞)) |
75 | | vex 3401 |
. . . . . . 7
⊢ 𝑏 ∈ V |
76 | | ifexg 4460 |
. . . . . . 7
⊢ ((𝑏 ∈ V ∧ 𝑅 ∈ ℝ*)
→ if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ∈ V) |
77 | 75, 21, 76 | sylancr 590 |
. . . . . 6
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ∈ V) |
78 | | breq1 5030 |
. . . . . . . 8
⊢ (𝑧 = 𝑏 → (𝑧 ≤ 𝑅 ↔ 𝑏 ≤ 𝑅)) |
79 | | id 22 |
. . . . . . . 8
⊢ (𝑧 = 𝑏 → 𝑧 = 𝑏) |
80 | 78, 79 | ifbieq1d 4435 |
. . . . . . 7
⊢ (𝑧 = 𝑏 → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) = if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) |
81 | 80, 32 | fvmptg 6767 |
. . . . . 6
⊢ ((𝑏 ∈ (0[,]+∞) ∧
if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ∈ V) → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑏) = if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) |
82 | 74, 77, 81 | syl2anr 600 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ ((𝑧 ∈
(0[,]+∞) ↦ if(𝑧
≤ 𝑅, 𝑧, 𝑅))‘𝑏) = if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) |
83 | 73, 82 | breq12d 5040 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (((𝑧 ∈
(0[,]+∞) ↦ if(𝑧
≤ 𝑅, 𝑧, 𝑅))‘𝑎) ≤ ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑏) ↔ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
84 | 72, 83 | sylibrd 262 |
. . 3
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑎 ≤ 𝑏 → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) ≤ ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑏))) |
85 | 57, 63 | xaddcld 12770 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑎
+𝑒 𝑏)
∈ ℝ*) |
86 | | xrmin1 12646 |
. . . . . . 7
⊢ (((𝑎 +𝑒 𝑏) ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑏)) |
87 | 85, 58, 86 | syl2anc 587 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑏)) |
88 | 85, 58 | ifcld 4457 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ∈
ℝ*) |
89 | 57, 58 | xaddcld 12770 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑎
+𝑒 𝑅)
∈ ℝ*) |
90 | | xrmin2 12647 |
. . . . . . . 8
⊢ (((𝑎 +𝑒 𝑏) ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ 𝑅) |
91 | 85, 58, 90 | syl2anc 587 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ 𝑅) |
92 | | xaddid2 12711 |
. . . . . . . . 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 12924 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (0[,]+∞) ↔
(𝑎 ∈
ℝ* ∧ 0 ≤ 𝑎)) |
96 | 95 | simprbi 500 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (0[,]+∞) → 0
≤ 𝑎) |
97 | 96 | ad2antrl 728 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 0 ≤ 𝑎) |
98 | | xleadd1a 12722 |
. . . . . . . . 9
⊢ (((0
∈ ℝ* ∧ 𝑎 ∈ ℝ* ∧ 𝑅 ∈ ℝ*)
∧ 0 ≤ 𝑎) → (0
+𝑒 𝑅)
≤ (𝑎
+𝑒 𝑅)) |
99 | 94, 57, 58, 97, 98 | syl31anc 1374 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (0 +𝑒 𝑅) ≤ (𝑎 +𝑒 𝑅)) |
100 | 93, 99 | eqbrtrrd 5051 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 𝑅 ≤ (𝑎 +𝑒 𝑅)) |
101 | 88, 58, 89, 91, 100 | xrletrd 12631 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑅)) |
102 | | oveq2 7172 |
. . . . . . . 8
⊢ (𝑏 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (𝑎 +𝑒 𝑏) = (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
103 | 102 | breq2d 5039 |
. . . . . . 7
⊢ (𝑏 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑏) ↔ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))) |
104 | | oveq2 7172 |
. . . . . . . 8
⊢ (𝑅 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (𝑎 +𝑒 𝑅) = (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
105 | 104 | breq2d 5039 |
. . . . . . 7
⊢ (𝑅 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑅) ↔ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))) |
106 | 103, 105 | ifboth 4450 |
. . . . . 6
⊢
((if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑏) ∧ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑅)) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
107 | 87, 101, 106 | syl2anc 587 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
108 | 63, 58 | ifcld 4457 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ∈
ℝ*) |
109 | 58, 108 | xaddcld 12770 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑅
+𝑒 if(𝑏
≤ 𝑅, 𝑏, 𝑅)) ∈
ℝ*) |
110 | 58 | xaddid1d 12712 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑅
+𝑒 0) = 𝑅) |
111 | | elxrge0 12924 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (0[,]+∞) ↔
(𝑏 ∈
ℝ* ∧ 0 ≤ 𝑏)) |
112 | 111 | simprbi 500 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (0[,]+∞) → 0
≤ 𝑏) |
113 | 112 | ad2antll 729 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 0 ≤ 𝑏) |
114 | 48 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 0 ≤ 𝑅) |
115 | | breq2 5031 |
. . . . . . . . . 10
⊢ (𝑏 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (0 ≤ 𝑏 ↔ 0 ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
116 | | breq2 5031 |
. . . . . . . . . 10
⊢ (𝑅 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (0 ≤ 𝑅 ↔ 0 ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
117 | 115, 116 | ifboth 4450 |
. . . . . . . . 9
⊢ ((0 ≤
𝑏 ∧ 0 ≤ 𝑅) → 0 ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) |
118 | 113, 114,
117 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 0 ≤ if(𝑏 ≤
𝑅, 𝑏, 𝑅)) |
119 | | xleadd2a 12723 |
. . . . . . . 8
⊢ (((0
∈ ℝ* ∧ if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ∈ ℝ* ∧ 𝑅 ∈ ℝ*)
∧ 0 ≤ if(𝑏 ≤
𝑅, 𝑏, 𝑅)) → (𝑅 +𝑒 0) ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
120 | 94, 108, 58, 118, 119 | syl31anc 1374 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑅
+𝑒 0) ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
121 | 110, 120 | eqbrtrrd 5051 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 𝑅 ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
122 | 88, 58, 109, 91, 121 | xrletrd 12631 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
123 | | oveq1 7171 |
. . . . . . 7
⊢ (𝑎 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) = (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
124 | 123 | breq2d 5039 |
. . . . . 6
⊢ (𝑎 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) ↔ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))) |
125 | | oveq1 7171 |
. . . . . . 7
⊢ (𝑅 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) = (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
126 | 125 | breq2d 5039 |
. . . . . 6
⊢ (𝑅 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) ↔ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))) |
127 | 124, 126 | ifboth 4450 |
. . . . 5
⊢
((if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) ∧ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
128 | 107, 122,
127 | syl2anc 587 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
129 | | ge0xaddcl 12929 |
. . . . 5
⊢ ((𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞))
→ (𝑎
+𝑒 𝑏)
∈ (0[,]+∞)) |
130 | | ovex 7197 |
. . . . . 6
⊢ (𝑎 +𝑒 𝑏) ∈ V |
131 | | ifexg 4460 |
. . . . . 6
⊢ (((𝑎 +𝑒 𝑏) ∈ V ∧ 𝑅 ∈ ℝ*)
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ∈ V) |
132 | 130, 21, 131 | sylancr 590 |
. . . . 5
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ∈ V) |
133 | | breq1 5030 |
. . . . . . 7
⊢ (𝑧 = (𝑎 +𝑒 𝑏) → (𝑧 ≤ 𝑅 ↔ (𝑎 +𝑒 𝑏) ≤ 𝑅)) |
134 | | id 22 |
. . . . . . 7
⊢ (𝑧 = (𝑎 +𝑒 𝑏) → 𝑧 = (𝑎 +𝑒 𝑏)) |
135 | 133, 134 | ifbieq1d 4435 |
. . . . . 6
⊢ (𝑧 = (𝑎 +𝑒 𝑏) → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) = if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅)) |
136 | 135, 32 | fvmptg 6767 |
. . . . 5
⊢ (((𝑎 +𝑒 𝑏) ∈ (0[,]+∞) ∧
if((𝑎 +𝑒
𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ∈ V) → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘(𝑎 +𝑒 𝑏)) = if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅)) |
137 | 129, 132,
136 | syl2anr 600 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ ((𝑧 ∈
(0[,]+∞) ↦ if(𝑧
≤ 𝑅, 𝑧, 𝑅))‘(𝑎 +𝑒 𝑏)) = if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅)) |
138 | 73, 82 | oveq12d 7182 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (((𝑧 ∈
(0[,]+∞) ↦ if(𝑧
≤ 𝑅, 𝑧, 𝑅))‘𝑎) +𝑒 ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑏)) = (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
139 | 128, 137,
138 | 3brtr4d 5059 |
. . 3
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ ((𝑧 ∈
(0[,]+∞) ↦ if(𝑧
≤ 𝑅, 𝑧, 𝑅))‘(𝑎 +𝑒 𝑏)) ≤ (((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) +𝑒 ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑏))) |
140 | 1, 24, 55, 84, 139 | comet 23259 |
. 2
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → ((𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) ∘ 𝐶) ∈ (∞Met‘𝑋)) |
141 | 19, 140 | eqeltrrd 2834 |
1
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐷 ∈ (∞Met‘𝑋)) |