Theorem stdbdxmet 22130

Description: The standard bounded metric is an extended metric given an extended metric and a positive extended real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.)

Hypothesis

Ref	Expression
stdbdmet.1	⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅))

Assertion

Ref	Expression
stdbdxmet	⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → 𝐷 ∈ (∞Met‘𝑋))

Distinct variable groups:   𝑥,𝑦,𝐶   𝑥,𝑅,𝑦   𝑥,𝑋,𝑦

Allowed substitution hints:   𝐷(𝑥,𝑦)

Proof of Theorem stdbdxmet

Dummy variables 𝑎 𝑏 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp1 1054	. . . . 5 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → 𝐶 ∈ (∞Met‘𝑋))
2		xmetcl 21946	. . . . . . 7 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐶𝑦) ∈ ℝ*)
3		xmetge0 21959	. . . . . . 7 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝑥𝐶𝑦))
4		elxrge0 12152	. . . . . . 7 ⊢ ((𝑥𝐶𝑦) ∈ (0[,]+∞) ↔ ((𝑥𝐶𝑦) ∈ ℝ* ∧ 0 ≤ (𝑥𝐶𝑦)))
5	2, 3, 4	sylanbrc 695	. . . . . 6 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐶𝑦) ∈ (0[,]+∞))
6	5	3expb 1258	. . . . 5 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ∈ (0[,]+∞))
7	1, 6	sylan 487	. . . 4 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ∈ (0[,]+∞))
8		xmetf 21944	. . . . . . 7 ⊢ (𝐶 ∈ (∞Met‘𝑋) → 𝐶:(𝑋 × 𝑋)⟶ℝ*)
9	8	3ad2ant1 1075	. . . . . 6 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → 𝐶:(𝑋 × 𝑋)⟶ℝ*)
10		ffn 5958	. . . . . 6 ⊢ (𝐶:(𝑋 × 𝑋)⟶ℝ* → 𝐶 Fn (𝑋 × 𝑋))
11	9, 10	syl 17	. . . . 5 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → 𝐶 Fn (𝑋 × 𝑋))
12		fnov 6666	. . . . 5 ⊢ (𝐶 Fn (𝑋 × 𝑋) ↔ 𝐶 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝐶𝑦)))
13	11, 12	sylib 207	. . . 4 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → 𝐶 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝐶𝑦)))
14		eqidd 2611	. . . 4 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → (𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) = (𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅)))
15		breq1 4586	. . . . 5 ⊢ (𝑧 = (𝑥𝐶𝑦) → (𝑧 ≤ 𝑅 ↔ (𝑥𝐶𝑦) ≤ 𝑅))
16		id 22	. . . . 5 ⊢ (𝑧 = (𝑥𝐶𝑦) → 𝑧 = (𝑥𝐶𝑦))
17	15, 16	ifbieq1d 4059	. . . 4 ⊢ (𝑧 = (𝑥𝐶𝑦) → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) = if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅))
18	7, 13, 14, 17	fmpt2co 7147	. . 3 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) ∘ 𝐶) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅)))
19		stdbdmet.1	. . 3 ⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅))
20	18, 19	syl6eqr 2662	. 2 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) ∘ 𝐶) = 𝐷)
21		elxrge0 12152	. . . . . 6 ⊢ (𝑧 ∈ (0[,]+∞) ↔ (𝑧 ∈ ℝ* ∧ 0 ≤ 𝑧))
22	21	simplbi 475	. . . . 5 ⊢ (𝑧 ∈ (0[,]+∞) → 𝑧 ∈ ℝ*)
23		simp2 1055	. . . . 5 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → 𝑅 ∈ ℝ*)
24		ifcl 4080	. . . . 5 ⊢ ((𝑧 ∈ ℝ* ∧ 𝑅 ∈ ℝ*) → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) ∈ ℝ*)
25	22, 23, 24	syl2anr 494	. . . 4 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ 𝑧 ∈ (0[,]+∞)) → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) ∈ ℝ*)
26		eqid 2610	. . . 4 ⊢ (𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) = (𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))
27	25, 26	fmptd 6292	. . 3 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → (𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅)):(0[,]+∞)⟶ℝ*)
28		id 22	. . . . . 6 ⊢ (𝑎 ∈ (0[,]+∞) → 𝑎 ∈ (0[,]+∞))
29		vex 3176	. . . . . . 7 ⊢ 𝑎 ∈ V
30		ifexg 4107	. . . . . . 7 ⊢ ((𝑎 ∈ V ∧ 𝑅 ∈ ℝ*) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈ V)
31	29, 23, 30	sylancr 694	. . . . . 6 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈ V)
32		breq1 4586	. . . . . . . 8 ⊢ (𝑧 = 𝑎 → (𝑧 ≤ 𝑅 ↔ 𝑎 ≤ 𝑅))
33		id 22	. . . . . . . 8 ⊢ (𝑧 = 𝑎 → 𝑧 = 𝑎)
34	32, 33	ifbieq1d 4059	. . . . . . 7 ⊢ (𝑧 = 𝑎 → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) = if(𝑎 ≤ 𝑅, 𝑎, 𝑅))
35	34, 26	fvmptg 6189	. . . . . 6 ⊢ ((𝑎 ∈ (0[,]+∞) ∧ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈ V) → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) = if(𝑎 ≤ 𝑅, 𝑎, 𝑅))
36	28, 31, 35	syl2anr 494	. . . . 5 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) = if(𝑎 ≤ 𝑅, 𝑎, 𝑅))
37	36	eqeq1d 2612	. . . 4 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → (((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) = 0 ↔ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0))
38		eqeq1 2614	. . . . . 6 ⊢ (𝑎 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (𝑎 = 0 ↔ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0))
39	38	bibi1d 332	. . . . 5 ⊢ (𝑎 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → ((𝑎 = 0 ↔ 𝑎 = 0) ↔ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0 ↔ 𝑎 = 0)))
40		eqeq1 2614	. . . . . 6 ⊢ (𝑅 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (𝑅 = 0 ↔ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0))
41	40	bibi1d 332	. . . . 5 ⊢ (𝑅 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → ((𝑅 = 0 ↔ 𝑎 = 0) ↔ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0 ↔ 𝑎 = 0)))
42		biidd 251	. . . . 5 ⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ 𝑎 ∈ (0[,]+∞)) ∧ 𝑎 ≤ 𝑅) → (𝑎 = 0 ↔ 𝑎 = 0))
43		simp3 1056	. . . . . . . . 9 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → 0 < 𝑅)
44	43	gt0ne0d 10471	. . . . . . . 8 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → 𝑅 ≠ 0)
45	44	neneqd 2787	. . . . . . 7 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → ¬ 𝑅 = 0)
46	45	ad2antrr 758	. . . . . 6 ⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ 𝑎 ∈ (0[,]+∞)) ∧ ¬ 𝑎 ≤ 𝑅) → ¬ 𝑅 = 0)
47		0xr 9965	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ*
48		xrltle 11858	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ* ∧ 𝑅 ∈ ℝ*) → (0 < 𝑅 → 0 ≤ 𝑅))
49	47, 23, 48	sylancr 694	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → (0 < 𝑅 → 0 ≤ 𝑅))
50	43, 49	mpd 15	. . . . . . . . 9 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → 0 ≤ 𝑅)
51	50	adantr 480	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → 0 ≤ 𝑅)
52		breq1 4586	. . . . . . . 8 ⊢ (𝑎 = 0 → (𝑎 ≤ 𝑅 ↔ 0 ≤ 𝑅))
53	51, 52	syl5ibrcom 236	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → (𝑎 = 0 → 𝑎 ≤ 𝑅))
54	53	con3dimp 456	. . . . . 6 ⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ 𝑎 ∈ (0[,]+∞)) ∧ ¬ 𝑎 ≤ 𝑅) → ¬ 𝑎 = 0)
55	46, 54	2falsed 365	. . . . 5 ⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ 𝑎 ∈ (0[,]+∞)) ∧ ¬ 𝑎 ≤ 𝑅) → (𝑅 = 0 ↔ 𝑎 = 0))
56	39, 41, 42, 55	ifbothda 4073	. . . 4 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) = 0 ↔ 𝑎 = 0))
57	37, 56	bitrd 267	. . 3 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ 𝑎 ∈ (0[,]+∞)) → (((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) = 0 ↔ 𝑎 = 0))
58		elxrge0 12152	. . . . . . . . . 10 ⊢ (𝑎 ∈ (0[,]+∞) ↔ (𝑎 ∈ ℝ* ∧ 0 ≤ 𝑎))
59	58	simplbi 475	. . . . . . . . 9 ⊢ (𝑎 ∈ (0[,]+∞) → 𝑎 ∈ ℝ*)
60	59	ad2antrl 760	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → 𝑎 ∈ ℝ*)
61	23	adantr 480	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → 𝑅 ∈ ℝ*)
62		xrmin1 11882	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ* ∧ 𝑅 ∈ ℝ*) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑎)
63	60, 61, 62	syl2anc 691	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑎)
64	60, 61	ifcld 4081	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈ ℝ*)
65		elxrge0 12152	. . . . . . . . . 10 ⊢ (𝑏 ∈ (0[,]+∞) ↔ (𝑏 ∈ ℝ* ∧ 0 ≤ 𝑏))
66	65	simplbi 475	. . . . . . . . 9 ⊢ (𝑏 ∈ (0[,]+∞) → 𝑏 ∈ ℝ*)
67	66	ad2antll 761	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → 𝑏 ∈ ℝ*)
68		xrletr 11865	. . . . . . . 8 ⊢ ((if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈ ℝ* ∧ 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*) → ((if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑎 ∧ 𝑎 ≤ 𝑏) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏))
69	64, 60, 67, 68	syl3anc 1318	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → ((if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑎 ∧ 𝑎 ≤ 𝑏) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏))
70	63, 69	mpand 707	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → (𝑎 ≤ 𝑏 → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏))
71		xrmin2 11883	. . . . . . 7 ⊢ ((𝑎 ∈ ℝ* ∧ 𝑅 ∈ ℝ*) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑅)
72	60, 61, 71	syl2anc 691	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑅)
73	70, 72	jctird 565	. . . . 5 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → (𝑎 ≤ 𝑏 → (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏 ∧ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑅)))
74		xrlemin 11889	. . . . . 6 ⊢ ((if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ∈ ℝ* ∧ 𝑏 ∈ ℝ* ∧ 𝑅 ∈ ℝ*) → (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ↔ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏 ∧ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑅)))
75	64, 67, 61, 74	syl3anc 1318	. . . . 5 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ↔ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑏 ∧ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ 𝑅)))
76	73, 75	sylibrd 248	. . . 4 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → (𝑎 ≤ 𝑏 → if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))
77	36	adantrr 749	. . . . 5 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) = if(𝑎 ≤ 𝑅, 𝑎, 𝑅))
78		simpr 476	. . . . . 6 ⊢ ((𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞)) → 𝑏 ∈ (0[,]+∞))
79		vex 3176	. . . . . . 7 ⊢ 𝑏 ∈ V
80		ifexg 4107	. . . . . . 7 ⊢ ((𝑏 ∈ V ∧ 𝑅 ∈ ℝ*) → if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ∈ V)
81	79, 23, 80	sylancr 694	. . . . . 6 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ∈ V)
82		breq1 4586	. . . . . . . 8 ⊢ (𝑧 = 𝑏 → (𝑧 ≤ 𝑅 ↔ 𝑏 ≤ 𝑅))
83		id 22	. . . . . . . 8 ⊢ (𝑧 = 𝑏 → 𝑧 = 𝑏)
84	82, 83	ifbieq1d 4059	. . . . . . 7 ⊢ (𝑧 = 𝑏 → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) = if(𝑏 ≤ 𝑅, 𝑏, 𝑅))
85	84, 26	fvmptg 6189	. . . . . 6 ⊢ ((𝑏 ∈ (0[,]+∞) ∧ if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ∈ V) → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑏) = if(𝑏 ≤ 𝑅, 𝑏, 𝑅))
86	78, 81, 85	syl2anr 494	. . . . 5 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑏) = if(𝑏 ≤ 𝑅, 𝑏, 𝑅))
87	77, 86	breq12d 4596	. . . 4 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → (((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) ≤ ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑏) ↔ if(𝑎 ≤ 𝑅, 𝑎, 𝑅) ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))
88	76, 87	sylibrd 248	. . 3 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → (𝑎 ≤ 𝑏 → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) ≤ ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑏)))
89	60, 67	xaddcld 12003	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → (𝑎 +𝑒 𝑏) ∈ ℝ*)
90		xrmin1 11882	. . . . . . 7 ⊢ (((𝑎 +𝑒 𝑏) ∈ ℝ* ∧ 𝑅 ∈ ℝ*) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑏))
91	89, 61, 90	syl2anc 691	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑏))
92	89, 61	ifcld 4081	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ∈ ℝ*)
93	60, 61	xaddcld 12003	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → (𝑎 +𝑒 𝑅) ∈ ℝ*)
94		xrmin2 11883	. . . . . . . 8 ⊢ (((𝑎 +𝑒 𝑏) ∈ ℝ* ∧ 𝑅 ∈ ℝ*) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ 𝑅)
95	89, 61, 94	syl2anc 691	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ 𝑅)
96		xaddid2 11947	. . . . . . . . 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 479	. . . . . . . . . 10 ⊢ (𝑎 ∈ (0[,]+∞) → 0 ≤ 𝑎)
100	99	ad2antrl 760	. . . . . . . . 9 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → 0 ≤ 𝑎)
101		xleadd1a 11955	. . . . . . . . 9 ⊢ (((0 ∈ ℝ* ∧ 𝑎 ∈ ℝ* ∧ 𝑅 ∈ ℝ*) ∧ 0 ≤ 𝑎) → (0 +𝑒 𝑅) ≤ (𝑎 +𝑒 𝑅))
102	98, 60, 61, 100, 101	syl31anc 1321	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → (0 +𝑒 𝑅) ≤ (𝑎 +𝑒 𝑅))
103	97, 102	eqbrtrrd 4607	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → 𝑅 ≤ (𝑎 +𝑒 𝑅))
104	92, 61, 93, 95, 103	xrletrd 11869	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑅))
105		oveq2 6557	. . . . . . . 8 ⊢ (𝑏 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (𝑎 +𝑒 𝑏) = (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))
106	105	breq2d 4595	. . . . . . 7 ⊢ (𝑏 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑏) ↔ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))))
107		oveq2 6557	. . . . . . . 8 ⊢ (𝑅 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (𝑎 +𝑒 𝑅) = (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))
108	107	breq2d 4595	. . . . . . 7 ⊢ (𝑅 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑅) ↔ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))))
109	106, 108	ifboth 4074	. . . . . 6 ⊢ ((if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑏) ∧ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 𝑅)) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))
110	91, 104, 109	syl2anc 691	. . . . 5 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))
111	67, 61	ifcld 4081	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ∈ ℝ*)
112	61, 111	xaddcld 12003	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) ∈ ℝ*)
113		xaddid1 11946	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ* → (𝑅 +𝑒 0) = 𝑅)
114	61, 113	syl 17	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → (𝑅 +𝑒 0) = 𝑅)
115	65	simprbi 479	. . . . . . . . . 10 ⊢ (𝑏 ∈ (0[,]+∞) → 0 ≤ 𝑏)
116	115	ad2antll 761	. . . . . . . . 9 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → 0 ≤ 𝑏)
117	50	adantr 480	. . . . . . . . 9 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → 0 ≤ 𝑅)
118		breq2 4587	. . . . . . . . . 10 ⊢ (𝑏 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (0 ≤ 𝑏 ↔ 0 ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))
119		breq2 4587	. . . . . . . . . 10 ⊢ (𝑅 = if(𝑏 ≤ 𝑅, 𝑏, 𝑅) → (0 ≤ 𝑅 ↔ 0 ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))
120	118, 119	ifboth 4074	. . . . . . . . 9 ⊢ ((0 ≤ 𝑏 ∧ 0 ≤ 𝑅) → 0 ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅))
121	116, 117, 120	syl2anc 691	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → 0 ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅))
122		xleadd2a 11956	. . . . . . . 8 ⊢ (((0 ∈ ℝ* ∧ if(𝑏 ≤ 𝑅, 𝑏, 𝑅) ∈ ℝ* ∧ 𝑅 ∈ ℝ*) ∧ 0 ≤ if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) → (𝑅 +𝑒 0) ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))
123	98, 111, 61, 121, 122	syl31anc 1321	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → (𝑅 +𝑒 0) ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))
124	114, 123	eqbrtrrd 4607	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → 𝑅 ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))
125	92, 61, 112, 95, 124	xrletrd 11869	. . . . 5 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))
126		oveq1 6556	. . . . . . 7 ⊢ (𝑎 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) = (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))
127	126	breq2d 4595	. . . . . 6 ⊢ (𝑎 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) ↔ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))))
128		oveq1 6556	. . . . . . 7 ⊢ (𝑅 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) = (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))
129	128	breq2d 4595	. . . . . 6 ⊢ (𝑅 = if(𝑎 ≤ 𝑅, 𝑎, 𝑅) → (if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) ↔ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))))
130	127, 129	ifboth 4074	. . . . 5 ⊢ ((if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑎 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)) ∧ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (𝑅 +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅))) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))
131	110, 125, 130	syl2anc 691	. . . 4 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ≤ (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))
132		ge0xaddcl 12157	. . . . 5 ⊢ ((𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞)) → (𝑎 +𝑒 𝑏) ∈ (0[,]+∞))
133		ovex 6577	. . . . . 6 ⊢ (𝑎 +𝑒 𝑏) ∈ V
134		ifexg 4107	. . . . . 6 ⊢ (((𝑎 +𝑒 𝑏) ∈ V ∧ 𝑅 ∈ ℝ*) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ∈ V)
135	133, 23, 134	sylancr 694	. . . . 5 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ∈ V)
136		breq1 4586	. . . . . . 7 ⊢ (𝑧 = (𝑎 +𝑒 𝑏) → (𝑧 ≤ 𝑅 ↔ (𝑎 +𝑒 𝑏) ≤ 𝑅))
137		id 22	. . . . . . 7 ⊢ (𝑧 = (𝑎 +𝑒 𝑏) → 𝑧 = (𝑎 +𝑒 𝑏))
138	136, 137	ifbieq1d 4059	. . . . . 6 ⊢ (𝑧 = (𝑎 +𝑒 𝑏) → if(𝑧 ≤ 𝑅, 𝑧, 𝑅) = if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅))
139	138, 26	fvmptg 6189	. . . . 5 ⊢ (((𝑎 +𝑒 𝑏) ∈ (0[,]+∞) ∧ if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅) ∈ V) → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘(𝑎 +𝑒 𝑏)) = if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅))
140	132, 135, 139	syl2anr 494	. . . 4 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘(𝑎 +𝑒 𝑏)) = if((𝑎 +𝑒 𝑏) ≤ 𝑅, (𝑎 +𝑒 𝑏), 𝑅))
141	77, 86	oveq12d 6567	. . . 4 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → (((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) +𝑒 ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑏)) = (if(𝑎 ≤ 𝑅, 𝑎, 𝑅) +𝑒 if(𝑏 ≤ 𝑅, 𝑏, 𝑅)))
142	131, 140, 141	3brtr4d 4615	. . 3 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑎 ∈ (0[,]+∞) ∧ 𝑏 ∈ (0[,]+∞))) → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘(𝑎 +𝑒 𝑏)) ≤ (((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑎) +𝑒 ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅))‘𝑏)))
143	1, 27, 57, 88, 142	comet 22128	. 2 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → ((𝑧 ∈ (0[,]+∞) ↦ if(𝑧 ≤ 𝑅, 𝑧, 𝑅)) ∘ 𝐶) ∈ (∞Met‘𝑋))
144	20, 143	eqeltrrd 2689	1 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → 𝐷 ∈ (∞Met‘𝑋))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  Vcvv 3173  ifcif 4036   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036   ∘ ccom 5042   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  0cc0 9815  +∞cpnf 9950  ℝ^*cxr 9952   < clt 9953   ≤ cle 9954   +_𝑒 cxad 11820  [,]cicc 12049  ∞Metcxmt 19552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-2 10956  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-icc 12053  df-xmet 19560

This theorem is referenced by:  stdbdmet  22131  stdbdbl  22132  stdbdmopn  22133