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	$⊢ D = (x \in X, y \in X ⟼ if (x C y \leq R, x C y, R))$
	Assertion	stdbdxmet	$⊢ (C \in ∞Met (X) \land R \in ℝ^{*} \land 0 < R) \to D \in ∞Met (X)$

Proof

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

Metamath Proof Explorer

Theorem stdbdxmet

Proof