metss2lem

	Ref	Expression
Hypotheses	metequiv.3	$⊢ J = MetOpen (C)$
	metequiv.4	$⊢ K = MetOpen (D)$
	metss2.1	$⊢ φ \to C \in Met (X)$
	metss2.2	$⊢ φ \to D \in Met (X)$
	metss2.3	$⊢ φ \to R \in ℝ^{+}$
	metss2.4	$⊢ (φ \land (x \in X \land y \in X)) \to x C y \leq R (x D y)$
Assertion	metss2lem	$⊢ (φ \land (x \in X \land S \in ℝ^{+})) \to x ball (D) (\frac{S}{R}) \subseteq x ball (C) S$

Proof

Step	Hyp	Ref	Expression
1		metequiv.3	$⊢ J = MetOpen (C)$
2		metequiv.4	$⊢ K = MetOpen (D)$
3		metss2.1	$⊢ φ \to C \in Met (X)$
4		metss2.2	$⊢ φ \to D \in Met (X)$
5		metss2.3	$⊢ φ \to R \in ℝ^{+}$
6		metss2.4	$⊢ (φ \land (x \in X \land y \in X)) \to x C y \leq R (x D y)$
7	4	ad2antrr	$⊢ ((φ \land (x \in X \land S \in ℝ^{+})) \land y \in X) \to D \in Met (X)$
8		simplrl	$⊢ ((φ \land (x \in X \land S \in ℝ^{+})) \land y \in X) \to x \in X$
9		simpr	$⊢ ((φ \land (x \in X \land S \in ℝ^{+})) \land y \in X) \to y \in X$
10		metcl	$⊢ (D \in Met (X) \land x \in X \land y \in X) \to x D y \in ℝ$
11	7 8 9 10	syl3anc	$⊢ ((φ \land (x \in X \land S \in ℝ^{+})) \land y \in X) \to x D y \in ℝ$
12		simplrr	$⊢ ((φ \land (x \in X \land S \in ℝ^{+})) \land y \in X) \to S \in ℝ^{+}$
13	12	rpred	$⊢ ((φ \land (x \in X \land S \in ℝ^{+})) \land y \in X) \to S \in ℝ$
14	5	ad2antrr	$⊢ ((φ \land (x \in X \land S \in ℝ^{+})) \land y \in X) \to R \in ℝ^{+}$
15	11 13 14	ltmuldiv2d	$⊢ ((φ \land (x \in X \land S \in ℝ^{+})) \land y \in X) \to (R (x D y) < S \leftrightarrow x D y < \frac{S}{R})$
16	6	anassrs	$⊢ ((φ \land x \in X) \land y \in X) \to x C y \leq R (x D y)$
17	16	adantlrr	$⊢ ((φ \land (x \in X \land S \in ℝ^{+})) \land y \in X) \to x C y \leq R (x D y)$
18	3	ad2antrr	$⊢ ((φ \land (x \in X \land S \in ℝ^{+})) \land y \in X) \to C \in Met (X)$
19		metcl	$⊢ (C \in Met (X) \land x \in X \land y \in X) \to x C y \in ℝ$
20	18 8 9 19	syl3anc	$⊢ ((φ \land (x \in X \land S \in ℝ^{+})) \land y \in X) \to x C y \in ℝ$
21	14	rpred	$⊢ ((φ \land (x \in X \land S \in ℝ^{+})) \land y \in X) \to R \in ℝ$
22	21 11	remulcld	$⊢ ((φ \land (x \in X \land S \in ℝ^{+})) \land y \in X) \to R (x D y) \in ℝ$
23		lelttr	$⊢ (x C y \in ℝ \land R (x D y) \in ℝ \land S \in ℝ) \to ((x C y \leq R (x D y) \land R (x D y) < S) \to x C y < S)$
24	20 22 13 23	syl3anc	$⊢ ((φ \land (x \in X \land S \in ℝ^{+})) \land y \in X) \to ((x C y \leq R (x D y) \land R (x D y) < S) \to x C y < S)$
25	17 24	mpand	$⊢ ((φ \land (x \in X \land S \in ℝ^{+})) \land y \in X) \to (R (x D y) < S \to x C y < S)$
26	15 25	sylbird	$⊢ ((φ \land (x \in X \land S \in ℝ^{+})) \land y \in X) \to (x D y < \frac{S}{R} \to x C y < S)$
27	26	ss2rabdv	$⊢ (φ \land (x \in X \land S \in ℝ^{+})) \to \{y \in X \| x D y < \frac{S}{R}\} \subseteq \{y \in X \| x C y < S\}$
28		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
29	4 28	syl	$⊢ φ \to D \in ∞Met (X)$
30	29	adantr	$⊢ (φ \land (x \in X \land S \in ℝ^{+})) \to D \in ∞Met (X)$
31		simprl	$⊢ (φ \land (x \in X \land S \in ℝ^{+})) \to x \in X$
32		simpr	$⊢ (x \in X \land S \in ℝ^{+}) \to S \in ℝ^{+}$
33		rpdivcl	$⊢ (S \in ℝ^{+} \land R \in ℝ^{+}) \to \frac{S}{R} \in ℝ^{+}$
34	32 5 33	syl2anr	$⊢ (φ \land (x \in X \land S \in ℝ^{+})) \to \frac{S}{R} \in ℝ^{+}$
35	34	rpxrd	$⊢ (φ \land (x \in X \land S \in ℝ^{+})) \to \frac{S}{R} \in ℝ^{*}$
36		blval	$⊢ (D \in ∞Met (X) \land x \in X \land \frac{S}{R} \in ℝ^{*}) \to x ball (D) (\frac{S}{R}) = \{y \in X \| x D y < \frac{S}{R}\}$
37	30 31 35 36	syl3anc	$⊢ (φ \land (x \in X \land S \in ℝ^{+})) \to x ball (D) (\frac{S}{R}) = \{y \in X \| x D y < \frac{S}{R}\}$
38		metxmet	$⊢ C \in Met (X) \to C \in ∞Met (X)$
39	3 38	syl	$⊢ φ \to C \in ∞Met (X)$
40	39	adantr	$⊢ (φ \land (x \in X \land S \in ℝ^{+})) \to C \in ∞Met (X)$
41		rpxr	$⊢ S \in ℝ^{+} \to S \in ℝ^{*}$
42	41	ad2antll	$⊢ (φ \land (x \in X \land S \in ℝ^{+})) \to S \in ℝ^{*}$
43		blval	$⊢ (C \in ∞Met (X) \land x \in X \land S \in ℝ^{*}) \to x ball (C) S = \{y \in X \| x C y < S\}$
44	40 31 42 43	syl3anc	$⊢ (φ \land (x \in X \land S \in ℝ^{+})) \to x ball (C) S = \{y \in X \| x C y < S\}$
45	27 37 44	3sstr4d	$⊢ (φ \land (x \in X \land S \in ℝ^{+})) \to x ball (D) (\frac{S}{R}) \subseteq x ball (C) S$

Metamath Proof Explorer

Theorem metss2lem

Proof