stdbdxmet

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)

		Ref	Expression
	Hypothesis	stdbdmet.1	⊢ 𝐷 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) )
	Assertion	stdbdxmet	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		stdbdmet.1	⊢ 𝐷 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) )
2		simp1	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
3		xmetcl	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐶 𝑦 ) ∈ ℝ^* )
4		xmetge0	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → 0 ≤ ( 𝑥 𝐶 𝑦 ) )
5		elxrge0	⊢ ( ( 𝑥 𝐶 𝑦 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝑥 𝐶 𝑦 ) ∈ ℝ^* ∧ 0 ≤ ( 𝑥 𝐶 𝑦 ) ) )
6	3 4 5	sylanbrc	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐶 𝑦 ) ∈ ( 0 [,] +∞ ) )
7	6	3expb	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐶 𝑦 ) ∈ ( 0 [,] +∞ ) )
8	2 7	sylan	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐶 𝑦 ) ∈ ( 0 [,] +∞ ) )
9		xmetf	⊢ ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) → 𝐶 : ( 𝑋 × 𝑋 ) ⟶ ℝ^* )
10	9	3ad2ant1	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → 𝐶 : ( 𝑋 × 𝑋 ) ⟶ ℝ^* )
11	10	ffnd	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → 𝐶 Fn ( 𝑋 × 𝑋 ) )
12		fnov	⊢ ( 𝐶 Fn ( 𝑋 × 𝑋 ) ↔ 𝐶 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐶 𝑦 ) ) )
13	11 12	sylib	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → 𝐶 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐶 𝑦 ) ) )
14		eqidd	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) = ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) )
15		breq1	⊢ ( 𝑧 = ( 𝑥 𝐶 𝑦 ) → ( 𝑧 ≤ 𝑅 ↔ ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 ) )
16		id	⊢ ( 𝑧 = ( 𝑥 𝐶 𝑦 ) → 𝑧 = ( 𝑥 𝐶 𝑦 ) )
17	15 16	ifbieq1d	⊢ ( 𝑧 = ( 𝑥 𝐶 𝑦 ) → if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) = if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) )
18	8 13 14 17	fmpoco	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) ∘ 𝐶 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) ) )
19	18 1	eqtr4di	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) ∘ 𝐶 ) = 𝐷 )
20		eliccxr	⊢ ( 𝑧 ∈ ( 0 [,] +∞ ) → 𝑧 ∈ ℝ^* )
21		simp2	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → 𝑅 ∈ ℝ^* )
22		ifcl	⊢ ( ( 𝑧 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ) → if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ∈ ℝ^* )
23	20 21 22	syl2anr	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ 𝑧 ∈ ( 0 [,] +∞ ) ) → if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ∈ ℝ^* )
24	23	fmpttd	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) : ( 0 [,] +∞ ) ⟶ ℝ^* )
25		id	⊢ ( 𝑎 ∈ ( 0 [,] +∞ ) → 𝑎 ∈ ( 0 [,] +∞ ) )
26		vex	⊢ 𝑎 ∈ V
27		ifexg	⊢ ( ( 𝑎 ∈ V ∧ 𝑅 ∈ ℝ^* ) → if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ∈ V )
28	26 21 27	sylancr	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ∈ V )
29		breq1	⊢ ( 𝑧 = 𝑎 → ( 𝑧 ≤ 𝑅 ↔ 𝑎 ≤ 𝑅 ) )
30		id	⊢ ( 𝑧 = 𝑎 → 𝑧 = 𝑎 )
31	29 30	ifbieq1d	⊢ ( 𝑧 = 𝑎 → if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) = if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) )
32		eqid	⊢ ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) = ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) )
33	31 32	fvmptg	⊢ ( ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ∈ V ) → ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) ‘ 𝑎 ) = if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) )
34	25 28 33	syl2anr	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ 𝑎 ∈ ( 0 [,] +∞ ) ) → ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) ‘ 𝑎 ) = if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) )
35	34	eqeq1d	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ 𝑎 ∈ ( 0 [,] +∞ ) ) → ( ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) ‘ 𝑎 ) = 0 ↔ if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) = 0 ) )
36		eqeq1	⊢ ( 𝑎 = if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) → ( 𝑎 = 0 ↔ if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) = 0 ) )
37	36	bibi1d	⊢ ( 𝑎 = if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) → ( ( 𝑎 = 0 ↔ 𝑎 = 0 ) ↔ ( if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) = 0 ↔ 𝑎 = 0 ) ) )
38		eqeq1	⊢ ( 𝑅 = if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) → ( 𝑅 = 0 ↔ if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) = 0 ) )
39	38	bibi1d	⊢ ( 𝑅 = if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) → ( ( 𝑅 = 0 ↔ 𝑎 = 0 ) ↔ ( if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) = 0 ↔ 𝑎 = 0 ) ) )
40		biidd	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ 𝑎 ∈ ( 0 [,] +∞ ) ) ∧ 𝑎 ≤ 𝑅 ) → ( 𝑎 = 0 ↔ 𝑎 = 0 ) )
41		simp3	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → 0 < 𝑅 )
42	41	gt0ne0d	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → 𝑅 ≠ 0 )
43	42	neneqd	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → ¬ 𝑅 = 0 )
44	43	ad2antrr	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ 𝑎 ∈ ( 0 [,] +∞ ) ) ∧ ¬ 𝑎 ≤ 𝑅 ) → ¬ 𝑅 = 0 )
45		0xr	⊢ 0 ∈ ℝ^*
46		xrltle	⊢ ( ( 0 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ) → ( 0 < 𝑅 → 0 ≤ 𝑅 ) )
47	45 21 46	sylancr	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → ( 0 < 𝑅 → 0 ≤ 𝑅 ) )
48	41 47	mpd	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → 0 ≤ 𝑅 )
49	48	adantr	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ 𝑎 ∈ ( 0 [,] +∞ ) ) → 0 ≤ 𝑅 )
50		breq1	⊢ ( 𝑎 = 0 → ( 𝑎 ≤ 𝑅 ↔ 0 ≤ 𝑅 ) )
51	49 50	syl5ibrcom	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ 𝑎 ∈ ( 0 [,] +∞ ) ) → ( 𝑎 = 0 → 𝑎 ≤ 𝑅 ) )
52	51	con3dimp	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ 𝑎 ∈ ( 0 [,] +∞ ) ) ∧ ¬ 𝑎 ≤ 𝑅 ) → ¬ 𝑎 = 0 )
53	44 52	2falsed	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ 𝑎 ∈ ( 0 [,] +∞ ) ) ∧ ¬ 𝑎 ≤ 𝑅 ) → ( 𝑅 = 0 ↔ 𝑎 = 0 ) )
54	37 39 40 53	ifbothda	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ 𝑎 ∈ ( 0 [,] +∞ ) ) → ( if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) = 0 ↔ 𝑎 = 0 ) )
55	35 54	bitrd	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ 𝑎 ∈ ( 0 [,] +∞ ) ) → ( ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) ‘ 𝑎 ) = 0 ↔ 𝑎 = 0 ) )
56		eliccxr	⊢ ( 𝑎 ∈ ( 0 [,] +∞ ) → 𝑎 ∈ ℝ^* )
57	56	ad2antrl	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → 𝑎 ∈ ℝ^* )
58	21	adantr	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → 𝑅 ∈ ℝ^* )
59		xrmin1	⊢ ( ( 𝑎 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ) → if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ≤ 𝑎 )
60	57 58 59	syl2anc	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ≤ 𝑎 )
61	57 58	ifcld	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ∈ ℝ^* )
62		eliccxr	⊢ ( 𝑏 ∈ ( 0 [,] +∞ ) → 𝑏 ∈ ℝ^* )
63	62	ad2antll	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → 𝑏 ∈ ℝ^* )
64		xrletr	⊢ ( ( if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ∈ ℝ^* ∧ 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) → ( ( if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ≤ 𝑎 ∧ 𝑎 ≤ 𝑏 ) → if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ≤ 𝑏 ) )
65	61 57 63 64	syl3anc	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → ( ( if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ≤ 𝑎 ∧ 𝑎 ≤ 𝑏 ) → if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ≤ 𝑏 ) )
66	60 65	mpand	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → ( 𝑎 ≤ 𝑏 → if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ≤ 𝑏 ) )
67		xrmin2	⊢ ( ( 𝑎 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ) → if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ≤ 𝑅 )
68	57 58 67	syl2anc	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ≤ 𝑅 )
69	66 68	jctird	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → ( 𝑎 ≤ 𝑏 → ( if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ≤ 𝑏 ∧ if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ≤ 𝑅 ) ) )
70		xrlemin	⊢ ( ( if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ) → ( if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ≤ if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ↔ ( if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ≤ 𝑏 ∧ if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ≤ 𝑅 ) ) )
71	61 63 58 70	syl3anc	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → ( if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ≤ if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ↔ ( if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ≤ 𝑏 ∧ if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ≤ 𝑅 ) ) )
72	69 71	sylibrd	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → ( 𝑎 ≤ 𝑏 → if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ≤ if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) )
73	34	adantrr	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) ‘ 𝑎 ) = if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) )
74		simpr	⊢ ( ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) → 𝑏 ∈ ( 0 [,] +∞ ) )
75		vex	⊢ 𝑏 ∈ V
76		ifexg	⊢ ( ( 𝑏 ∈ V ∧ 𝑅 ∈ ℝ^* ) → if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ∈ V )
77	75 21 76	sylancr	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ∈ V )
78		breq1	⊢ ( 𝑧 = 𝑏 → ( 𝑧 ≤ 𝑅 ↔ 𝑏 ≤ 𝑅 ) )
79		id	⊢ ( 𝑧 = 𝑏 → 𝑧 = 𝑏 )
80	78 79	ifbieq1d	⊢ ( 𝑧 = 𝑏 → if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) = if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) )
81	80 32	fvmptg	⊢ ( ( 𝑏 ∈ ( 0 [,] +∞ ) ∧ if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ∈ V ) → ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) ‘ 𝑏 ) = if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) )
82	74 77 81	syl2anr	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) ‘ 𝑏 ) = if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) )
83	73 82	breq12d	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → ( ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) ‘ 𝑎 ) ≤ ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) ‘ 𝑏 ) ↔ if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) ≤ if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) )
84	72 83	sylibrd	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → ( 𝑎 ≤ 𝑏 → ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) ‘ 𝑎 ) ≤ ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) ‘ 𝑏 ) ) )
85	57 63	xaddcld	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → ( 𝑎 +_𝑒 𝑏 ) ∈ ℝ^* )
86		xrmin1	⊢ ( ( ( 𝑎 +_𝑒 𝑏 ) ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ) → if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ ( 𝑎 +_𝑒 𝑏 ) )
87	85 58 86	syl2anc	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ ( 𝑎 +_𝑒 𝑏 ) )
88	85 58	ifcld	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ∈ ℝ^* )
89	57 58	xaddcld	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → ( 𝑎 +_𝑒 𝑅 ) ∈ ℝ^* )
90		xrmin2	⊢ ( ( ( 𝑎 +_𝑒 𝑏 ) ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ) → if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ 𝑅 )
91	85 58 90	syl2anc	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ 𝑅 )
92		xaddlid	⊢ ( 𝑅 ∈ ℝ^* → ( 0 +_𝑒 𝑅 ) = 𝑅 )
93	58 92	syl	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → ( 0 +_𝑒 𝑅 ) = 𝑅 )
94	45	a1i	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → 0 ∈ ℝ^* )
95		elxrge0	⊢ ( 𝑎 ∈ ( 0 [,] +∞ ) ↔ ( 𝑎 ∈ ℝ^* ∧ 0 ≤ 𝑎 ) )
96	95	simprbi	⊢ ( 𝑎 ∈ ( 0 [,] +∞ ) → 0 ≤ 𝑎 )
97	96	ad2antrl	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → 0 ≤ 𝑎 )
98		xleadd1a	⊢ ( ( ( 0 ∈ ℝ^* ∧ 𝑎 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ) ∧ 0 ≤ 𝑎 ) → ( 0 +_𝑒 𝑅 ) ≤ ( 𝑎 +_𝑒 𝑅 ) )
99	94 57 58 97 98	syl31anc	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → ( 0 +_𝑒 𝑅 ) ≤ ( 𝑎 +_𝑒 𝑅 ) )
100	93 99	eqbrtrrd	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → 𝑅 ≤ ( 𝑎 +_𝑒 𝑅 ) )
101	88 58 89 91 100	xrletrd	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ ( 𝑎 +_𝑒 𝑅 ) )
102		oveq2	⊢ ( 𝑏 = if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) → ( 𝑎 +_𝑒 𝑏 ) = ( 𝑎 +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) )
103	102	breq2d	⊢ ( 𝑏 = if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) → ( if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ ( 𝑎 +_𝑒 𝑏 ) ↔ if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ ( 𝑎 +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) ) )
104		oveq2	⊢ ( 𝑅 = if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) → ( 𝑎 +_𝑒 𝑅 ) = ( 𝑎 +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) )
105	104	breq2d	⊢ ( 𝑅 = if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) → ( if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ ( 𝑎 +_𝑒 𝑅 ) ↔ if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ ( 𝑎 +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) ) )
106	103 105	ifboth	⊢ ( ( if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ ( 𝑎 +_𝑒 𝑏 ) ∧ if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ ( 𝑎 +_𝑒 𝑅 ) ) → if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ ( 𝑎 +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) )
107	87 101 106	syl2anc	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ ( 𝑎 +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) )
108	63 58	ifcld	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ∈ ℝ^* )
109	58 108	xaddcld	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → ( 𝑅 +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) ∈ ℝ^* )
110	58	xaddridd	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → ( 𝑅 +_𝑒 0 ) = 𝑅 )
111		elxrge0	⊢ ( 𝑏 ∈ ( 0 [,] +∞ ) ↔ ( 𝑏 ∈ ℝ^* ∧ 0 ≤ 𝑏 ) )
112	111	simprbi	⊢ ( 𝑏 ∈ ( 0 [,] +∞ ) → 0 ≤ 𝑏 )
113	112	ad2antll	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → 0 ≤ 𝑏 )
114	48	adantr	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → 0 ≤ 𝑅 )
115		breq2	⊢ ( 𝑏 = if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) → ( 0 ≤ 𝑏 ↔ 0 ≤ if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) )
116		breq2	⊢ ( 𝑅 = if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) → ( 0 ≤ 𝑅 ↔ 0 ≤ if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) )
117	115 116	ifboth	⊢ ( ( 0 ≤ 𝑏 ∧ 0 ≤ 𝑅 ) → 0 ≤ if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) )
118	113 114 117	syl2anc	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → 0 ≤ if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) )
119		xleadd2a	⊢ ( ( ( 0 ∈ ℝ^* ∧ if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ) ∧ 0 ≤ if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) → ( 𝑅 +_𝑒 0 ) ≤ ( 𝑅 +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) )
120	94 108 58 118 119	syl31anc	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → ( 𝑅 +_𝑒 0 ) ≤ ( 𝑅 +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) )
121	110 120	eqbrtrrd	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → 𝑅 ≤ ( 𝑅 +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) )
122	88 58 109 91 121	xrletrd	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ ( 𝑅 +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) )
123		oveq1	⊢ ( 𝑎 = if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) → ( 𝑎 +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) = ( if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) )
124	123	breq2d	⊢ ( 𝑎 = if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) → ( if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ ( 𝑎 +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) ↔ if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ ( if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) ) )
125		oveq1	⊢ ( 𝑅 = if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) → ( 𝑅 +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) = ( if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) )
126	125	breq2d	⊢ ( 𝑅 = if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) → ( if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ ( 𝑅 +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) ↔ if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ ( if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) ) )
127	124 126	ifboth	⊢ ( ( if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ ( 𝑎 +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) ∧ if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ ( 𝑅 +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) ) → if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ ( if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) )
128	107 122 127	syl2anc	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ≤ ( if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) )
129		ge0xaddcl	⊢ ( ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) → ( 𝑎 +_𝑒 𝑏 ) ∈ ( 0 [,] +∞ ) )
130		ovex	⊢ ( 𝑎 +_𝑒 𝑏 ) ∈ V
131		ifexg	⊢ ( ( ( 𝑎 +_𝑒 𝑏 ) ∈ V ∧ 𝑅 ∈ ℝ^* ) → if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ∈ V )
132	130 21 131	sylancr	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ∈ V )
133		breq1	⊢ ( 𝑧 = ( 𝑎 +_𝑒 𝑏 ) → ( 𝑧 ≤ 𝑅 ↔ ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 ) )
134		id	⊢ ( 𝑧 = ( 𝑎 +_𝑒 𝑏 ) → 𝑧 = ( 𝑎 +_𝑒 𝑏 ) )
135	133 134	ifbieq1d	⊢ ( 𝑧 = ( 𝑎 +_𝑒 𝑏 ) → if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) = if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) )
136	135 32	fvmptg	⊢ ( ( ( 𝑎 +_𝑒 𝑏 ) ∈ ( 0 [,] +∞ ) ∧ if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) ∈ V ) → ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) ‘ ( 𝑎 +_𝑒 𝑏 ) ) = if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) )
137	129 132 136	syl2anr	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) ‘ ( 𝑎 +_𝑒 𝑏 ) ) = if ( ( 𝑎 +_𝑒 𝑏 ) ≤ 𝑅 , ( 𝑎 +_𝑒 𝑏 ) , 𝑅 ) )
138	73 82	oveq12d	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → ( ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) ‘ 𝑎 ) +_𝑒 ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) ‘ 𝑏 ) ) = ( if ( 𝑎 ≤ 𝑅 , 𝑎 , 𝑅 ) +_𝑒 if ( 𝑏 ≤ 𝑅 , 𝑏 , 𝑅 ) ) )
139	128 137 138	3brtr4d	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) ) → ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) ‘ ( 𝑎 +_𝑒 𝑏 ) ) ≤ ( ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) ‘ 𝑎 ) +_𝑒 ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) ‘ 𝑏 ) ) )
140	2 24 55 84 139	comet	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → ( ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 ≤ 𝑅 , 𝑧 , 𝑅 ) ) ∘ 𝐶 ) ∈ ( ∞Met ‘ 𝑋 ) )
141	19 140	eqeltrrd	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )

Metamath Proof Explorer

Theorem stdbdxmet

Proof