lebnumlem2

Description: Lemma for lebnum . As a finite sum of point-to-set distance functions, which are continuous by metdscn , the function F is also continuous. (Contributed by Mario Carneiro, 14-Feb-2015) (Revised by AV, 30-Sep-2020)

	Ref	Expression
Hypotheses	lebnum.j	$⊢ J = MetOpen (D)$
	lebnum.d	$⊢ φ \to D \in Met (X)$
	lebnum.c	$⊢ φ \to J \in Comp$
	lebnum.s	$⊢ φ \to U \subseteq J$
	lebnum.u	$⊢ φ \to X = ⋃ U$
	lebnumlem1.u	$⊢ φ \to U \in Fin$
	lebnumlem1.n	$⊢ φ \to \neg X \in U$
	lebnumlem1.f	$⊢ F = (y \in X ⟼ \sum_{k \in U} inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <))$
	lebnumlem2.k	$⊢ K = topGen (ran (.))$
Assertion	lebnumlem2	$⊢ φ \to F \in (J Cn K)$

Proof

Step	Hyp	Ref	Expression
1		lebnum.j	$⊢ J = MetOpen (D)$
2		lebnum.d	$⊢ φ \to D \in Met (X)$
3		lebnum.c	$⊢ φ \to J \in Comp$
4		lebnum.s	$⊢ φ \to U \subseteq J$
5		lebnum.u	$⊢ φ \to X = ⋃ U$
6		lebnumlem1.u	$⊢ φ \to U \in Fin$
7		lebnumlem1.n	$⊢ φ \to \neg X \in U$
8		lebnumlem1.f	$⊢ F = (y \in X ⟼ \sum_{k \in U} inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <))$
9		lebnumlem2.k	$⊢ K = topGen (ran (.))$
10		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
11		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
12	2 11	syl	$⊢ φ \to D \in ∞Met (X)$
13	1	mopntopon	$⊢ D \in ∞Met (X) \to J \in TopOn (X)$
14	12 13	syl	$⊢ φ \to J \in TopOn (X)$
15	2	adantr	$⊢ (φ \land k \in U) \to D \in Met (X)$
16		difssd	$⊢ (φ \land k \in U) \to X ∖ k \subseteq X$
17	12	adantr	$⊢ (φ \land k \in U) \to D \in ∞Met (X)$
18	17 13	syl	$⊢ (φ \land k \in U) \to J \in TopOn (X)$
19	4	sselda	$⊢ (φ \land k \in U) \to k \in J$
20		toponss	$⊢ (J \in TopOn (X) \land k \in J) \to k \subseteq X$
21	18 19 20	syl2anc	$⊢ (φ \land k \in U) \to k \subseteq X$
22		eleq1	$⊢ k = X \to (k \in U \leftrightarrow X \in U)$
23	22	notbid	$⊢ k = X \to (\neg k \in U \leftrightarrow \neg X \in U)$
24	7 23	syl5ibrcom	$⊢ φ \to (k = X \to \neg k \in U)$
25	24	necon2ad	$⊢ φ \to (k \in U \to k \neq X)$
26	25	imp	$⊢ (φ \land k \in U) \to k \neq X$
27		pssdifn0	$⊢ (k \subseteq X \land k \neq X) \to X ∖ k \neq \emptyset$
28	21 26 27	syl2anc	$⊢ (φ \land k \in U) \to X ∖ k \neq \emptyset$
29		eqid	$⊢ (y \in X ⟼ inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <)) = (y \in X ⟼ inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <))$
30	29 1 10	metdscn2	$⊢ (D \in Met (X) \land X ∖ k \subseteq X \land X ∖ k \neq \emptyset) \to (y \in X ⟼ inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <)) \in (J Cn TopOpen (ℂ_{fld}))$
31	15 16 28 30	syl3anc	$⊢ (φ \land k \in U) \to (y \in X ⟼ inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <)) \in (J Cn TopOpen (ℂ_{fld}))$
32	10 14 6 31	fsumcn	$⊢ φ \to (y \in X ⟼ \sum_{k \in U} inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <)) \in (J Cn TopOpen (ℂ_{fld}))$
33	8 32	eqeltrid	$⊢ φ \to F \in (J Cn TopOpen (ℂ_{fld}))$
34	10	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
35	34	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
36	1 2 3 4 5 6 7 8	lebnumlem1	$⊢ φ \to F : X ⟶ ℝ^{+}$
37	36	frnd	$⊢ φ \to ran F \subseteq ℝ^{+}$
38		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
39	37 38	sstrdi	$⊢ φ \to ran F \subseteq ℝ$
40		ax-resscn	$⊢ ℝ \subseteq ℂ$
41	40	a1i	$⊢ φ \to ℝ \subseteq ℂ$
42		cnrest2	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land ran F \subseteq ℝ \land ℝ \subseteq ℂ) \to (F \in (J Cn TopOpen (ℂ_{fld})) \leftrightarrow F \in (J Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)))$
43	35 39 41 42	syl3anc	$⊢ φ \to (F \in (J Cn TopOpen (ℂ_{fld})) \leftrightarrow F \in (J Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)))$
44	33 43	mpbid	$⊢ φ \to F \in (J Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ))$
45		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
46	9 45	eqtri	$⊢ K = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
47	46	oveq2i	$⊢ J Cn K = J Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
48	44 47	eleqtrrdi	$⊢ φ \to F \in (J Cn K)$

Metamath Proof Explorer

Theorem lebnumlem2

Proof