Step | Hyp | Ref
| Expression |
1 | | simp1 1061 |
. . . . 5
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐶 ∈ (∞Met‘𝑋)) |
2 | | xmetcl 22136 |
. . . . . . 7
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐶𝑦) ∈
ℝ*) |
3 | | xmetge0 22149 |
. . . . . . 7
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝑥𝐶𝑦)) |
4 | | elxrge0 12281 |
. . . . . . 7
⊢ ((𝑥𝐶𝑦) ∈ (0[,]+∞) ↔ ((𝑥𝐶𝑦) ∈ ℝ* ∧ 0 ≤
(𝑥𝐶𝑦))) |
5 | 2, 3, 4 | sylanbrc 698 |
. . . . . 6
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐶𝑦) ∈ (0[,]+∞)) |
6 | 5 | 3expb 1266 |
. . . . 5
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ∈ (0[,]+∞)) |
7 | 1, 6 | sylan 488 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ∈ (0[,]+∞)) |
8 | | xmetf 22134 |
. . . . . . 7
⊢ (𝐶 ∈ (∞Met‘𝑋) → 𝐶:(𝑋 × 𝑋)⟶ℝ*) |
9 | 8 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐶:(𝑋 × 𝑋)⟶ℝ*) |
10 | | ffn 6045 |
. . . . . 6
⊢ (𝐶:(𝑋 × 𝑋)⟶ℝ* → 𝐶 Fn (𝑋 × 𝑋)) |
11 | 9, 10 | syl 17 |
. . . . 5
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐶 Fn (𝑋 × 𝑋)) |
12 | | fnov 6768 |
. . . . 5
⊢ (𝐶 Fn (𝑋 × 𝑋) ↔ 𝐶 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝐶𝑦))) |
13 | 11, 12 | sylib 208 |
. . . 4
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐶 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝐶𝑦))) |
14 | | eqidd 2623 |
. . . 4
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → (𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) = (𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))) |
15 | | breq1 4656 |
. . . . 5
⊢ (𝑧 = (𝑥𝐶𝑦) → (𝑧 ≤ 𝑅 ↔ (𝑥𝐶𝑦) ≤ 𝑅)) |
16 | | id 22 |
. . . . 5
⊢ (𝑧 = (𝑥𝐶𝑦) → 𝑧 = (𝑥𝐶𝑦)) |
17 | 15, 16 | ifbieq1d 4109 |
. . . 4
⊢ (𝑧 = (𝑥𝐶𝑦) → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) = if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅)) |
18 | 7, 13, 14, 17 | fmpt2co 7260 |
. . 3
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → ((𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) ∘ 𝐶) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅))) |
19 | | stdbdmet.1 |
. . 3
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅)) |
20 | 18, 19 | syl6eqr 2674 |
. 2
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → ((𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) ∘ 𝐶) = 𝐷) |
21 | | elxrge0 12281 |
. . . . . 6
⊢ (𝑧 ∈ (0[,]+∞) ↔
(𝑧 ∈
ℝ* ∧ 0 ≤ 𝑧)) |
22 | 21 | simplbi 476 |
. . . . 5
⊢ (𝑧 ∈ (0[,]+∞) →
𝑧 ∈
ℝ*) |
23 | | simp2 1062 |
. . . . 5
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝑅 ∈
ℝ*) |
24 | | ifcl 4130 |
. . . . 5
⊢ ((𝑧 ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) ∈
ℝ*) |
25 | 22, 23, 24 | syl2anr 495 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑧 ∈ (0[,]+∞)) → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) ∈
ℝ*) |
26 | | eqid 2622 |
. . . 4
⊢ (𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) = (𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) |
27 | 25, 26 | fmptd 6385 |
. . 3
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → (𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅)):(0[,]+∞)⟶ℝ*) |
28 | | id 22 |
. . . . . 6
⊢ (𝑎 ∈ (0[,]+∞) →
𝑎 ∈
(0[,]+∞)) |
29 | | vex 3203 |
. . . . . . 7
⊢ 𝑎 ∈ V |
30 | | ifexg 4157 |
. . . . . . 7
⊢ ((𝑎 ∈ V ∧ 𝑅 ∈ ℝ*)
→ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈ V) |
31 | 29, 23, 30 | sylancr 695 |
. . . . . 6
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈ V) |
32 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑧 = 𝑎 → (𝑧 ≤ 𝑅 ↔ 𝑎 ≤ 𝑅)) |
33 | | id 22 |
. . . . . . . 8
⊢ (𝑧 = 𝑎 → 𝑧 = 𝑎) |
34 | 32, 33 | ifbieq1d 4109 |
. . . . . . 7
⊢ (𝑧 = 𝑎 → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) = if(𝑎 ≤ 𝑅, 𝑎, 𝑅)) |
35 | 34, 26 | fvmptg 6280 |
. . . . . 6
⊢ ((𝑎 ∈ (0[,]+∞) ∧
if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈ V) → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) = if(𝑎 ≤ 𝑅, 𝑎, 𝑅)) |
36 | 28, 31, 35 | syl2anr 495 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → ((𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) = if(𝑎 ≤ 𝑅, 𝑎, 𝑅)) |
37 | 36 | eqeq1d 2624 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → (((𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) = 0 ↔ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0)) |
38 | | eqeq1 2626 |
. . . . . 6
⊢ (𝑎 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (𝑎 = 0 ↔ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0)) |
39 | 38 | bibi1d 333 |
. . . . 5
⊢ (𝑎 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → ((𝑎 = 0 ↔ 𝑎 = 0) ↔ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0 ↔ 𝑎 = 0))) |
40 | | eqeq1 2626 |
. . . . . 6
⊢ (𝑅 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (𝑅 = 0 ↔ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0)) |
41 | 40 | bibi1d 333 |
. . . . 5
⊢ (𝑅 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → ((𝑅 = 0 ↔ 𝑎 = 0) ↔ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0 ↔ 𝑎 = 0))) |
42 | | biidd 252 |
. . . . 5
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) ∧ 𝑎 ≤ 𝑅) → (𝑎 = 0 ↔ 𝑎 = 0)) |
43 | | simp3 1063 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 0 < 𝑅) |
44 | 43 | gt0ne0d 10592 |
. . . . . . . 8
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝑅 ≠ 0) |
45 | 44 | neneqd 2799 |
. . . . . . 7
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → ¬ 𝑅 = 0) |
46 | 45 | ad2antrr 762 |
. . . . . 6
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) ∧ ¬ 𝑎 ≤ 𝑅) → ¬ 𝑅 = 0) |
47 | | 0xr 10086 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
48 | | xrltle 11982 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ 𝑅 ∈ ℝ*) → (0 <
𝑅 → 0 ≤ 𝑅)) |
49 | 47, 23, 48 | sylancr 695 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → (0 < 𝑅 → 0 ≤ 𝑅)) |
50 | 43, 49 | mpd 15 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 0 ≤ 𝑅) |
51 | 50 | adantr 481 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → 0 ≤ 𝑅) |
52 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑎 = 0 → (𝑎 ≤ 𝑅 ↔ 0 ≤ 𝑅)) |
53 | 51, 52 | syl5ibrcom 237 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → (𝑎 = 0 → 𝑎 ≤ 𝑅)) |
54 | 53 | con3dimp 457 |
. . . . . 6
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) ∧ ¬ 𝑎 ≤ 𝑅) → ¬ 𝑎 = 0) |
55 | 46, 54 | 2falsed 366 |
. . . . 5
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) ∧ ¬ 𝑎 ≤ 𝑅) → (𝑅 = 0 ↔ 𝑎 = 0)) |
56 | 39, 41, 42, 55 | ifbothda 4123 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0 ↔ 𝑎 = 0)) |
57 | 37, 56 | bitrd 268 |
. . 3
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → (((𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) = 0 ↔ 𝑎 = 0)) |
58 | | elxrge0 12281 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (0[,]+∞) ↔
(𝑎 ∈
ℝ* ∧ 0 ≤ 𝑎)) |
59 | 58 | simplbi 476 |
. . . . . . . . 9
⊢ (𝑎 ∈ (0[,]+∞) →
𝑎 ∈
ℝ*) |
60 | 59 | ad2antrl 764 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 𝑎 ∈
ℝ*) |
61 | 23 | adantr 481 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 𝑅 ∈
ℝ*) |
62 | | xrmin1 12008 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑎) |
63 | 60, 61, 62 | syl2anc 693 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑎) |
64 | 60, 61 | ifcld 4131 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈
ℝ*) |
65 | | elxrge0 12281 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (0[,]+∞) ↔
(𝑏 ∈
ℝ* ∧ 0 ≤ 𝑏)) |
66 | 65 | simplbi 476 |
. . . . . . . . 9
⊢ (𝑏 ∈ (0[,]+∞) →
𝑏 ∈
ℝ*) |
67 | 66 | ad2antll 765 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 𝑏 ∈
ℝ*) |
68 | | xrletr 11989 |
. . . . . . . 8
⊢
((if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈ ℝ* ∧ 𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → ((if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑎 ∧ 𝑎 ≤ 𝑏) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏)) |
69 | 64, 60, 67, 68 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ ((if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑎 ∧ 𝑎 ≤ 𝑏) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏)) |
70 | 63, 69 | mpand 711 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑎 ≤ 𝑏 → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏)) |
71 | | xrmin2 12009 |
. . . . . . 7
⊢ ((𝑎 ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑅) |
72 | 60, 61, 71 | syl2anc 693 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑅) |
73 | 70, 72 | jctird 567 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑎 ≤ 𝑏 → (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏 ∧ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑅))) |
74 | | xrlemin 12015 |
. . . . . 6
⊢
((if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈ ℝ* ∧ 𝑏 ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ↔ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏 ∧ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑅))) |
75 | 64, 67, 61, 74 | syl3anc 1326 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ↔ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏 ∧ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑅))) |
76 | 73, 75 | sylibrd 249 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑎 ≤ 𝑏 → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
77 | 36 | adantrr 753 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ ((𝑧 ∈
(0[,]+∞) ↦ if(𝑧
≤ 𝑅, 𝑧, 𝑅))‘𝑎) = if(𝑎 ≤ 𝑅, 𝑎, 𝑅)) |
78 | | simpr 477 |
. . . . . 6
⊢ ((𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞))
→ 𝑏 ∈
(0[,]+∞)) |
79 | | vex 3203 |
. . . . . . 7
⊢ 𝑏 ∈ V |
80 | | ifexg 4157 |
. . . . . . 7
⊢ ((𝑏 ∈ V ∧ 𝑅 ∈ ℝ*)
→ if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ∈ V) |
81 | 79, 23, 80 | sylancr 695 |
. . . . . 6
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ∈ V) |
82 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑧 = 𝑏 → (𝑧 ≤ 𝑅 ↔ 𝑏 ≤ 𝑅)) |
83 | | id 22 |
. . . . . . . 8
⊢ (𝑧 = 𝑏 → 𝑧 = 𝑏) |
84 | 82, 83 | ifbieq1d 4109 |
. . . . . . 7
⊢ (𝑧 = 𝑏 → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) = if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) |
85 | 84, 26 | fvmptg 6280 |
. . . . . 6
⊢ ((𝑏 ∈ (0[,]+∞) ∧
if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ∈ V) → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑏) = if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) |
86 | 78, 81, 85 | syl2anr 495 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ ((𝑧 ∈
(0[,]+∞) ↦ if(𝑧
≤ 𝑅, 𝑧, 𝑅))‘𝑏) = if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) |
87 | 77, 86 | breq12d 4666 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (((𝑧 ∈
(0[,]+∞) ↦ if(𝑧
≤ 𝑅, 𝑧, 𝑅))‘𝑎) ≤ ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑏) ↔ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
88 | 76, 87 | sylibrd 249 |
. . 3
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑎 ≤ 𝑏 → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) ≤ ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑏))) |
89 | 60, 67 | xaddcld 12131 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑎
+𝑒 𝑏)
∈ ℝ*) |
90 | | xrmin1 12008 |
. . . . . . 7
⊢ (((𝑎 +𝑒 𝑏) ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑏)) |
91 | 89, 61, 90 | syl2anc 693 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑏)) |
92 | 89, 61 | ifcld 4131 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ∈
ℝ*) |
93 | 60, 61 | xaddcld 12131 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑎
+𝑒 𝑅)
∈ ℝ*) |
94 | | xrmin2 12009 |
. . . . . . . 8
⊢ (((𝑎 +𝑒 𝑏) ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ 𝑅) |
95 | 89, 61, 94 | syl2anc 693 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ 𝑅) |
96 | | xaddid2 12073 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ*
→ (0 +𝑒 𝑅) = 𝑅) |
97 | 61, 96 | syl 17 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (0 +𝑒 𝑅) = 𝑅) |
98 | 47 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 0 ∈ ℝ*) |
99 | 58 | simprbi 480 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (0[,]+∞) → 0
≤ 𝑎) |
100 | 99 | ad2antrl 764 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 0 ≤ 𝑎) |
101 | | xleadd1a 12083 |
. . . . . . . . 9
⊢ (((0
∈ ℝ* ∧ 𝑎 ∈ ℝ* ∧ 𝑅 ∈ ℝ*)
∧ 0 ≤ 𝑎) → (0
+𝑒 𝑅)
≤ (𝑎
+𝑒 𝑅)) |
102 | 98, 60, 61, 100, 101 | syl31anc 1329 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (0 +𝑒 𝑅) ≤ (𝑎 +𝑒 𝑅)) |
103 | 97, 102 | eqbrtrrd 4677 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 𝑅 ≤ (𝑎 +𝑒 𝑅)) |
104 | 92, 61, 93, 95, 103 | xrletrd 11993 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑅)) |
105 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑏 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (𝑎 +𝑒 𝑏) = (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
106 | 105 | breq2d 4665 |
. . . . . . 7
⊢ (𝑏 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑏) ↔ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))) |
107 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑅 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (𝑎 +𝑒 𝑅) = (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
108 | 107 | breq2d 4665 |
. . . . . . 7
⊢ (𝑅 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑅) ↔ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))) |
109 | 106, 108 | ifboth 4124 |
. . . . . 6
⊢
((if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑏) ∧ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑅)) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
110 | 91, 104, 109 | syl2anc 693 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
111 | 67, 61 | ifcld 4131 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ∈
ℝ*) |
112 | 61, 111 | xaddcld 12131 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑅
+𝑒 if(𝑏
≤ 𝑅, 𝑏, 𝑅)) ∈
ℝ*) |
113 | | xaddid1 12072 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ*
→ (𝑅
+𝑒 0) = 𝑅) |
114 | 61, 113 | syl 17 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑅
+𝑒 0) = 𝑅) |
115 | 65 | simprbi 480 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (0[,]+∞) → 0
≤ 𝑏) |
116 | 115 | ad2antll 765 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 0 ≤ 𝑏) |
117 | 50 | adantr 481 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 0 ≤ 𝑅) |
118 | | breq2 4657 |
. . . . . . . . . 10
⊢ (𝑏 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (0 ≤ 𝑏 ↔ 0 ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
119 | | breq2 4657 |
. . . . . . . . . 10
⊢ (𝑅 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (0 ≤ 𝑅 ↔ 0 ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
120 | 118, 119 | ifboth 4124 |
. . . . . . . . 9
⊢ ((0 ≤
𝑏 ∧ 0 ≤ 𝑅) → 0 ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) |
121 | 116, 117,
120 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 0 ≤ if(𝑏 ≤
𝑅, 𝑏, 𝑅)) |
122 | | xleadd2a 12084 |
. . . . . . . 8
⊢ (((0
∈ ℝ* ∧ if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ∈ ℝ* ∧ 𝑅 ∈ ℝ*)
∧ 0 ≤ if(𝑏 ≤
𝑅, 𝑏, 𝑅)) → (𝑅 +𝑒 0) ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
123 | 98, 111, 61, 121, 122 | syl31anc 1329 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (𝑅
+𝑒 0) ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
124 | 114, 123 | eqbrtrrd 4677 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ 𝑅 ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
125 | 92, 61, 112, 95, 124 | xrletrd 11993 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
126 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑎 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) = (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
127 | 126 | breq2d 4665 |
. . . . . 6
⊢ (𝑎 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) ↔ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))) |
128 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑅 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) = (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
129 | 128 | breq2d 4665 |
. . . . . 6
⊢ (𝑅 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) ↔ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))) |
130 | 127, 129 | ifboth 4124 |
. . . . 5
⊢
((if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) ∧ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
131 | 110, 125,
130 | syl2anc 693 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
132 | | ge0xaddcl 12286 |
. . . . 5
⊢ ((𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞))
→ (𝑎
+𝑒 𝑏)
∈ (0[,]+∞)) |
133 | | ovex 6678 |
. . . . . 6
⊢ (𝑎 +𝑒 𝑏) ∈ V |
134 | | ifexg 4157 |
. . . . . 6
⊢ (((𝑎 +𝑒 𝑏) ∈ V ∧ 𝑅 ∈ ℝ*)
→ if((𝑎
+𝑒 𝑏)
≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ∈ V) |
135 | 133, 23, 134 | sylancr 695 |
. . . . 5
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ∈ V) |
136 | | breq1 4656 |
. . . . . . 7
⊢ (𝑧 = (𝑎 +𝑒 𝑏) → (𝑧 ≤ 𝑅 ↔ (𝑎 +𝑒 𝑏) ≤ 𝑅)) |
137 | | id 22 |
. . . . . . 7
⊢ (𝑧 = (𝑎 +𝑒 𝑏) → 𝑧 = (𝑎 +𝑒 𝑏)) |
138 | 136, 137 | ifbieq1d 4109 |
. . . . . 6
⊢ (𝑧 = (𝑎 +𝑒 𝑏) → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) = if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅)) |
139 | 138, 26 | fvmptg 6280 |
. . . . 5
⊢ (((𝑎 +𝑒 𝑏) ∈ (0[,]+∞) ∧
if((𝑎 +𝑒
𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ∈ V) → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘(𝑎 +𝑒 𝑏)) = if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅)) |
140 | 132, 135,
139 | syl2anr 495 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ ((𝑧 ∈
(0[,]+∞) ↦ if(𝑧
≤ 𝑅, 𝑧, 𝑅))‘(𝑎 +𝑒 𝑏)) = if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅)) |
141 | 77, 86 | oveq12d 6668 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ (((𝑧 ∈
(0[,]+∞) ↦ if(𝑧
≤ 𝑅, 𝑧, 𝑅))‘𝑎) +𝑒 ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑏)) = (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) |
142 | 131, 140,
141 | 3brtr4d 4685 |
. . 3
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧
𝑏 ∈ (0[,]+∞)))
→ ((𝑧 ∈
(0[,]+∞) ↦ if(𝑧
≤ 𝑅, 𝑧, 𝑅))‘(𝑎 +𝑒 𝑏)) ≤ (((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) +𝑒 ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑏))) |
143 | 1, 27, 57, 88, 142 | comet 22318 |
. 2
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → ((𝑧 ∈ (0[,]+∞) ↦
if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) ∘ 𝐶) ∈ (∞Met‘𝑋)) |
144 | 20, 143 | eqeltrrd 2702 |
1
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐷 ∈ (∞Met‘𝑋)) |