metdstri

Description: A generalization of the triangle inequality to the point-set distance function. Under the usual notation where the same symbol d denotes the point-point and point-set distance functions, this theorem would be written d ( a , S ) <_ d ( a , b ) + d ( b , S ) . (Contributed by Mario Carneiro, 4-Sep-2015)

		Ref	Expression
	Hypothesis	metdscn.f	$⊢ F = (x \in X ⟼ inf (ran (y \in S ⟼ x D y) ℝ^{*} <))$
	Assertion	metdstri	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to F (A) \leq (A D B) +_{𝑒} F (B)$

Proof

Step	Hyp	Ref	Expression
1		metdscn.f	$⊢ F = (x \in X ⟼ inf (ran (y \in S ⟼ x D y) ℝ^{*} <))$
2		simprr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) \in ℝ)) \to F (A) \in ℝ$
3		simprl	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) \in ℝ)) \to A D B \in ℝ$
4		rexsub	$⊢ (F (A) \in ℝ \land A D B \in ℝ) \to F (A) +_{𝑒} (- (A D B)) = F (A) - (A D B)$
5	2 3 4	syl2anc	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) \in ℝ)) \to F (A) +_{𝑒} (- (A D B)) = F (A) - (A D B)$
6	5	oveq2d	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) \in ℝ)) \to B ball (D) (F (A) +_{𝑒} (- (A D B))) = B ball (D) (F (A) - (A D B))$
7		simpll	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to D \in ∞Met (X)$
8	7	adantr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) \in ℝ)) \to D \in ∞Met (X)$
9		simprr	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to B \in X$
10	9	adantr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) \in ℝ)) \to B \in X$
11		simprl	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to A \in X$
12	11	adantr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) \in ℝ)) \to A \in X$
13	2 3	resubcld	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) \in ℝ)) \to F (A) - (A D B) \in ℝ$
14	3	leidd	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) \in ℝ)) \to A D B \leq A D B$
15		xmetsym	$⊢ (D \in ∞Met (X) \land A \in X \land B \in X) \to A D B = B D A$
16	7 11 9 15	syl3anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to A D B = B D A$
17	16	adantr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) \in ℝ)) \to A D B = B D A$
18	17	eqcomd	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) \in ℝ)) \to B D A = A D B$
19	2	recnd	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) \in ℝ)) \to F (A) \in ℂ$
20	3	recnd	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) \in ℝ)) \to A D B \in ℂ$
21	19 20	nncand	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) \in ℝ)) \to F (A) - (F (A) - (A D B)) = A D B$
22	14 18 21	3brtr4d	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) \in ℝ)) \to B D A \leq F (A) - (F (A) - (A D B))$
23		blss2	$⊢ ((D \in ∞Met (X) \land B \in X \land A \in X) \land (F (A) - (A D B) \in ℝ \land F (A) \in ℝ \land B D A \leq F (A) - (F (A) - (A D B)))) \to B ball (D) (F (A) - (A D B)) \subseteq A ball (D) F (A)$
24	8 10 12 13 2 22 23	syl33anc	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) \in ℝ)) \to B ball (D) (F (A) - (A D B)) \subseteq A ball (D) F (A)$
25	6 24	eqsstrd	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) \in ℝ)) \to B ball (D) (F (A) +_{𝑒} (- (A D B))) \subseteq A ball (D) F (A)$
26	25	expr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land A D B \in ℝ) \to (F (A) \in ℝ \to B ball (D) (F (A) +_{𝑒} (- (A D B))) \subseteq A ball (D) F (A))$
27	7	adantr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) = +∞)) \to D \in ∞Met (X)$
28	9	adantr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) = +∞)) \to B \in X$
29	1	metdsf	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to F : X ⟶ [0, +∞]$
30	29	adantr	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to F : X ⟶ [0, +∞]$
31	30 11	ffvelcdmd	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to F (A) \in [0, +∞]$
32		eliccxr	$⊢ F (A) \in [0, +∞] \to F (A) \in ℝ^{*}$
33	31 32	syl	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to F (A) \in ℝ^{*}$
34	33	adantr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land A D B \in ℝ) \to F (A) \in ℝ^{*}$
35		xmetcl	$⊢ (D \in ∞Met (X) \land A \in X \land B \in X) \to A D B \in ℝ^{*}$
36	7 11 9 35	syl3anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to A D B \in ℝ^{*}$
37	36	adantr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land A D B \in ℝ) \to A D B \in ℝ^{*}$
38	37	xnegcld	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land A D B \in ℝ) \to - (A D B) \in ℝ^{*}$
39	34 38	xaddcld	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land A D B \in ℝ) \to F (A) +_{𝑒} (- (A D B)) \in ℝ^{*}$
40	39	adantrr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) = +∞)) \to F (A) +_{𝑒} (- (A D B)) \in ℝ^{*}$
41		pnfxr	$⊢ +∞ \in ℝ^{*}$
42	41	a1i	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) = +∞)) \to +∞ \in ℝ^{*}$
43		pnfge	$⊢ F (A) +_{𝑒} (- (A D B)) \in ℝ^{*} \to F (A) +_{𝑒} (- (A D B)) \leq +∞$
44	40 43	syl	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) = +∞)) \to F (A) +_{𝑒} (- (A D B)) \leq +∞$
45		ssbl	$⊢ ((D \in ∞Met (X) \land B \in X) \land (F (A) +_{𝑒} (- (A D B)) \in ℝ^{} \land +∞ \in ℝ^{}) \land F (A) +_{𝑒} (- (A D B)) \leq +∞) \to B ball (D) (F (A) +_{𝑒} (- (A D B))) \subseteq B ball (D) +∞$
46	27 28 40 42 44 45	syl221anc	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) = +∞)) \to B ball (D) (F (A) +_{𝑒} (- (A D B))) \subseteq B ball (D) +∞$
47		simprr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) = +∞)) \to F (A) = +∞$
48	47	oveq2d	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) = +∞)) \to A ball (D) F (A) = A ball (D) +∞$
49	11	adantr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) = +∞)) \to A \in X$
50		simprl	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) = +∞)) \to A D B \in ℝ$
51		xblpnf	$⊢ (D \in ∞Met (X) \land A \in X) \to (B \in (A ball (D) +∞) \leftrightarrow (B \in X \land A D B \in ℝ))$
52	27 49 51	syl2anc	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) = +∞)) \to (B \in (A ball (D) +∞) \leftrightarrow (B \in X \land A D B \in ℝ))$
53	28 50 52	mpbir2and	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) = +∞)) \to B \in (A ball (D) +∞)$
54		blpnfctr	$⊢ (D \in ∞Met (X) \land A \in X \land B \in (A ball (D) +∞)) \to A ball (D) +∞ = B ball (D) +∞$
55	27 49 53 54	syl3anc	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) = +∞)) \to A ball (D) +∞ = B ball (D) +∞$
56	48 55	eqtr2d	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) = +∞)) \to B ball (D) +∞ = A ball (D) F (A)$
57	46 56	sseqtrd	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land (A D B \in ℝ \land F (A) = +∞)) \to B ball (D) (F (A) +_{𝑒} (- (A D B))) \subseteq A ball (D) F (A)$
58	57	expr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land A D B \in ℝ) \to (F (A) = +∞ \to B ball (D) (F (A) +_{𝑒} (- (A D B))) \subseteq A ball (D) F (A))$
59		elxrge0	$⊢ F (A) \in [0, +∞] \leftrightarrow (F (A) \in ℝ^{*} \land 0 \leq F (A))$
60	59	simprbi	$⊢ F (A) \in [0, +∞] \to 0 \leq F (A)$
61	31 60	syl	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to 0 \leq F (A)$
62		ge0nemnf	$⊢ (F (A) \in ℝ^{*} \land 0 \leq F (A)) \to F (A) \neq −∞$
63	33 61 62	syl2anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to F (A) \neq −∞$
64	33 63	jca	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to (F (A) \in ℝ^{*} \land F (A) \neq −∞)$
65	64	adantr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land A D B \in ℝ) \to (F (A) \in ℝ^{*} \land F (A) \neq −∞)$
66		xrnemnf	$⊢ (F (A) \in ℝ^{*} \land F (A) \neq −∞) \leftrightarrow (F (A) \in ℝ \lor F (A) = +∞)$
67	65 66	sylib	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land A D B \in ℝ) \to (F (A) \in ℝ \lor F (A) = +∞)$
68	26 58 67	mpjaod	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land A D B \in ℝ) \to B ball (D) (F (A) +_{𝑒} (- (A D B))) \subseteq A ball (D) F (A)$
69		pnfnlt	$⊢ F (A) \in ℝ^{*} \to \neg +∞ < F (A)$
70	33 69	syl	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to \neg +∞ < F (A)$
71	70	adantr	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land A D B = +∞) \to \neg +∞ < F (A)$
72	36	xnegcld	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to - (A D B) \in ℝ^{*}$
73	33 72	xaddcld	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to F (A) +_{𝑒} (- (A D B)) \in ℝ^{*}$
74		xbln0	$⊢ (D \in ∞Met (X) \land B \in X \land F (A) +_{𝑒} (- (A D B)) \in ℝ^{*}) \to (B ball (D) (F (A) +_{𝑒} (- (A D B))) \neq \emptyset \leftrightarrow 0 < F (A) +_{𝑒} (- (A D B)))$
75	7 9 73 74	syl3anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to (B ball (D) (F (A) +_{𝑒} (- (A D B))) \neq \emptyset \leftrightarrow 0 < F (A) +_{𝑒} (- (A D B)))$
76		xposdif	$⊢ (A D B \in ℝ^{} \land F (A) \in ℝ^{}) \to (A D B < F (A) \leftrightarrow 0 < F (A) +_{𝑒} (- (A D B)))$
77	36 33 76	syl2anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to (A D B < F (A) \leftrightarrow 0 < F (A) +_{𝑒} (- (A D B)))$
78	75 77	bitr4d	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to (B ball (D) (F (A) +_{𝑒} (- (A D B))) \neq \emptyset \leftrightarrow A D B < F (A))$
79		breq1	$⊢ A D B = +∞ \to (A D B < F (A) \leftrightarrow +∞ < F (A))$
80	78 79	sylan9bb	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land A D B = +∞) \to (B ball (D) (F (A) +_{𝑒} (- (A D B))) \neq \emptyset \leftrightarrow +∞ < F (A))$
81	80	necon1bbid	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land A D B = +∞) \to (\neg +∞ < F (A) \leftrightarrow B ball (D) (F (A) +_{𝑒} (- (A D B))) = \emptyset)$
82	71 81	mpbid	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land A D B = +∞) \to B ball (D) (F (A) +_{𝑒} (- (A D B))) = \emptyset$
83		0ss	$⊢ \emptyset \subseteq A ball (D) F (A)$
84	82 83	eqsstrdi	$⊢ (((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \land A D B = +∞) \to B ball (D) (F (A) +_{𝑒} (- (A D B))) \subseteq A ball (D) F (A)$
85		xmetge0	$⊢ (D \in ∞Met (X) \land A \in X \land B \in X) \to 0 \leq A D B$
86	7 11 9 85	syl3anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to 0 \leq A D B$
87		ge0nemnf	$⊢ (A D B \in ℝ^{*} \land 0 \leq A D B) \to A D B \neq −∞$
88	36 86 87	syl2anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to A D B \neq −∞$
89	36 88	jca	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to (A D B \in ℝ^{*} \land A D B \neq −∞)$
90		xrnemnf	$⊢ (A D B \in ℝ^{*} \land A D B \neq −∞) \leftrightarrow (A D B \in ℝ \lor A D B = +∞)$
91	89 90	sylib	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to (A D B \in ℝ \lor A D B = +∞)$
92	68 84 91	mpjaodan	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to B ball (D) (F (A) +_{𝑒} (- (A D B))) \subseteq A ball (D) F (A)$
93		sslin	$⊢ B ball (D) (F (A) +_{𝑒} (- (A D B))) \subseteq A ball (D) F (A) \to S \cap (B ball (D) (F (A) +_{𝑒} (- (A D B)))) \subseteq S \cap (A ball (D) F (A))$
94	92 93	syl	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to S \cap (B ball (D) (F (A) +_{𝑒} (- (A D B)))) \subseteq S \cap (A ball (D) F (A))$
95	33	xrleidd	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to F (A) \leq F (A)$
96		simplr	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to S \subseteq X$
97	1	metdsge	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land A \in X) \land F (A) \in ℝ^{*}) \to (F (A) \leq F (A) \leftrightarrow S \cap (A ball (D) F (A)) = \emptyset)$
98	7 96 11 33 97	syl31anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to (F (A) \leq F (A) \leftrightarrow S \cap (A ball (D) F (A)) = \emptyset)$
99	95 98	mpbid	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to S \cap (A ball (D) F (A)) = \emptyset$
100		sseq0	$⊢ (S \cap (B ball (D) (F (A) +_{𝑒} (- (A D B)))) \subseteq S \cap (A ball (D) F (A)) \land S \cap (A ball (D) F (A)) = \emptyset) \to S \cap (B ball (D) (F (A) +_{𝑒} (- (A D B)))) = \emptyset$
101	94 99 100	syl2anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to S \cap (B ball (D) (F (A) +_{𝑒} (- (A D B)))) = \emptyset$
102	1	metdsge	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land B \in X) \land F (A) +_{𝑒} (- (A D B)) \in ℝ^{*}) \to (F (A) +_{𝑒} (- (A D B)) \leq F (B) \leftrightarrow S \cap (B ball (D) (F (A) +_{𝑒} (- (A D B)))) = \emptyset)$
103	7 96 9 73 102	syl31anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to (F (A) +_{𝑒} (- (A D B)) \leq F (B) \leftrightarrow S \cap (B ball (D) (F (A) +_{𝑒} (- (A D B)))) = \emptyset)$
104	101 103	mpbird	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to F (A) +_{𝑒} (- (A D B)) \leq F (B)$
105	30 9	ffvelcdmd	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to F (B) \in [0, +∞]$
106		eliccxr	$⊢ F (B) \in [0, +∞] \to F (B) \in ℝ^{*}$
107	105 106	syl	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to F (B) \in ℝ^{*}$
108		elxrge0	$⊢ F (B) \in [0, +∞] \leftrightarrow (F (B) \in ℝ^{*} \land 0 \leq F (B))$
109	108	simprbi	$⊢ F (B) \in [0, +∞] \to 0 \leq F (B)$
110	105 109	syl	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to 0 \leq F (B)$
111		xlesubadd	$⊢ ((F (A) \in ℝ^{} \land A D B \in ℝ^{} \land F (B) \in ℝ^{*}) \land (0 \leq F (A) \land A D B \neq −∞ \land 0 \leq F (B))) \to (F (A) +_{𝑒} (- (A D B)) \leq F (B) \leftrightarrow F (A) \leq F (B) +_{𝑒} (A D B))$
112	33 36 107 61 88 110 111	syl33anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to (F (A) +_{𝑒} (- (A D B)) \leq F (B) \leftrightarrow F (A) \leq F (B) +_{𝑒} (A D B))$
113	104 112	mpbid	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to F (A) \leq F (B) +_{𝑒} (A D B)$
114		xaddcom	$⊢ (F (B) \in ℝ^{} \land A D B \in ℝ^{}) \to F (B) +_{𝑒} (A D B) = (A D B) +_{𝑒} F (B)$
115	107 36 114	syl2anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to F (B) +_{𝑒} (A D B) = (A D B) +_{𝑒} F (B)$
116	113 115	breqtrd	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to F (A) \leq (A D B) +_{𝑒} F (B)$

Metamath Proof Explorer

Theorem metdstri

Proof