metnrmlem1

	Ref	Expression
Hypotheses	metdscn.f	$⊢ F = (x \in X ⟼ inf (ran (y \in S ⟼ x D y) ℝ^{*} <))$
	metdscn.j	$⊢ J = MetOpen (D)$
	metnrmlem.1	$⊢ φ \to D \in ∞Met (X)$
	metnrmlem.2	$⊢ φ \to S \in Clsd (J)$
	metnrmlem.3	$⊢ φ \to T \in Clsd (J)$
	metnrmlem.4	$⊢ φ \to S \cap T = \emptyset$
Assertion	metnrmlem1	$⊢ (φ \land (A \in S \land B \in T)) \to if (1 \leq F (B), 1, F (B)) \leq A D B$

Proof

Step	Hyp	Ref	Expression
1		metdscn.f	$⊢ F = (x \in X ⟼ inf (ran (y \in S ⟼ x D y) ℝ^{*} <))$
2		metdscn.j	$⊢ J = MetOpen (D)$
3		metnrmlem.1	$⊢ φ \to D \in ∞Met (X)$
4		metnrmlem.2	$⊢ φ \to S \in Clsd (J)$
5		metnrmlem.3	$⊢ φ \to T \in Clsd (J)$
6		metnrmlem.4	$⊢ φ \to S \cap T = \emptyset$
7		1xr	$⊢ 1 \in ℝ^{*}$
8	3	adantr	$⊢ (φ \land (A \in S \land B \in T)) \to D \in ∞Met (X)$
9	4	adantr	$⊢ (φ \land (A \in S \land B \in T)) \to S \in Clsd (J)$
10		eqid	$⊢ ⋃ J = ⋃ J$
11	10	cldss	$⊢ S \in Clsd (J) \to S \subseteq ⋃ J$
12	9 11	syl	$⊢ (φ \land (A \in S \land B \in T)) \to S \subseteq ⋃ J$
13	2	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
14	8 13	syl	$⊢ (φ \land (A \in S \land B \in T)) \to X = ⋃ J$
15	12 14	sseqtrrd	$⊢ (φ \land (A \in S \land B \in T)) \to S \subseteq X$
16	1	metdsf	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to F : X ⟶ [0, +∞]$
17	8 15 16	syl2anc	$⊢ (φ \land (A \in S \land B \in T)) \to F : X ⟶ [0, +∞]$
18	5	adantr	$⊢ (φ \land (A \in S \land B \in T)) \to T \in Clsd (J)$
19	10	cldss	$⊢ T \in Clsd (J) \to T \subseteq ⋃ J$
20	18 19	syl	$⊢ (φ \land (A \in S \land B \in T)) \to T \subseteq ⋃ J$
21	20 14	sseqtrrd	$⊢ (φ \land (A \in S \land B \in T)) \to T \subseteq X$
22		simprr	$⊢ (φ \land (A \in S \land B \in T)) \to B \in T$
23	21 22	sseldd	$⊢ (φ \land (A \in S \land B \in T)) \to B \in X$
24	17 23	ffvelcdmd	$⊢ (φ \land (A \in S \land B \in T)) \to F (B) \in [0, +∞]$
25		eliccxr	$⊢ F (B) \in [0, +∞] \to F (B) \in ℝ^{*}$
26	24 25	syl	$⊢ (φ \land (A \in S \land B \in T)) \to F (B) \in ℝ^{*}$
27		ifcl	$⊢ (1 \in ℝ^{} \land F (B) \in ℝ^{}) \to if (1 \leq F (B), 1, F (B)) \in ℝ^{*}$
28	7 26 27	sylancr	$⊢ (φ \land (A \in S \land B \in T)) \to if (1 \leq F (B), 1, F (B)) \in ℝ^{*}$
29		simprl	$⊢ (φ \land (A \in S \land B \in T)) \to A \in S$
30	15 29	sseldd	$⊢ (φ \land (A \in S \land B \in T)) \to A \in X$
31		xmetcl	$⊢ (D \in ∞Met (X) \land A \in X \land B \in X) \to A D B \in ℝ^{*}$
32	8 30 23 31	syl3anc	$⊢ (φ \land (A \in S \land B \in T)) \to A D B \in ℝ^{*}$
33		xrmin2	$⊢ (1 \in ℝ^{} \land F (B) \in ℝ^{}) \to if (1 \leq F (B), 1, F (B)) \leq F (B)$
34	7 26 33	sylancr	$⊢ (φ \land (A \in S \land B \in T)) \to if (1 \leq F (B), 1, F (B)) \leq F (B)$
35	1	metdstri	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (B \in X \land A \in X)) \to F (B) \leq (B D A) +_{𝑒} F (A)$
36	8 15 23 30 35	syl22anc	$⊢ (φ \land (A \in S \land B \in T)) \to F (B) \leq (B D A) +_{𝑒} F (A)$
37		xmetsym	$⊢ (D \in ∞Met (X) \land B \in X \land A \in X) \to B D A = A D B$
38	8 23 30 37	syl3anc	$⊢ (φ \land (A \in S \land B \in T)) \to B D A = A D B$
39	1	metds0	$⊢ (D \in ∞Met (X) \land S \subseteq X \land A \in S) \to F (A) = 0$
40	8 15 29 39	syl3anc	$⊢ (φ \land (A \in S \land B \in T)) \to F (A) = 0$
41	38 40	oveq12d	$⊢ (φ \land (A \in S \land B \in T)) \to (B D A) +_{𝑒} F (A) = (A D B) +_{𝑒} 0$
42	32	xaddridd	$⊢ (φ \land (A \in S \land B \in T)) \to (A D B) +_{𝑒} 0 = A D B$
43	41 42	eqtrd	$⊢ (φ \land (A \in S \land B \in T)) \to (B D A) +_{𝑒} F (A) = A D B$
44	36 43	breqtrd	$⊢ (φ \land (A \in S \land B \in T)) \to F (B) \leq A D B$
45	28 26 32 34 44	xrletrd	$⊢ (φ \land (A \in S \land B \in T)) \to if (1 \leq F (B), 1, F (B)) \leq A D B$

Metamath Proof Explorer

Theorem metnrmlem1

Proof