Metamath Proof Explorer

Theorem 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 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
lebnum.d ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
lebnum.c ⊢ ( 𝜑 → 𝐽 ∈ Comp )
lebnum.s ⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 )
lebnum.u ⊢ ( 𝜑 → 𝑋 = ∪ 𝑈 )
lebnumlem1.u ⊢ ( 𝜑 → 𝑈 ∈ Fin )
lebnumlem1.n ⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
lebnumlem1.f ⊢ 𝐹 = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑈 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) )
lebnumlem2.k ⊢ 𝐾 = ( topGen ‘ ran (,) )
Assertion lebnumlem2 ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 lebnum.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 lebnum.d ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
3 lebnum.c ⊢ ( 𝜑 → 𝐽 ∈ Comp )
4 lebnum.s ⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 )
5 lebnum.u ⊢ ( 𝜑 → 𝑋 = ∪ 𝑈 )
6 lebnumlem1.u ⊢ ( 𝜑 → 𝑈 ∈ Fin )
7 lebnumlem1.n ⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
8 lebnumlem1.f ⊢ 𝐹 = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑈 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) )
9 lebnumlem2.k ⊢ 𝐾 = ( topGen ‘ ran (,) )
10 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
11 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
12 2 11 syl ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
13 1 mopntopon ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
14 12 13 syl ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
15 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
16 difssd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → ( 𝑋 ∖ 𝑘 ) ⊆ 𝑋 )
17 12 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
18 17 13 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
19 4 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝑘 ∈ 𝐽 )
20 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑘 ∈ 𝐽 ) → 𝑘 ⊆ 𝑋 )
21 18 19 20 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝑘 ⊆ 𝑋 )
22 eleq1 ⊢ ( 𝑘 = 𝑋 → ( 𝑘 ∈ 𝑈 ↔ 𝑋 ∈ 𝑈 ) )
23 22 notbid ⊢ ( 𝑘 = 𝑋 → ( ¬ 𝑘 ∈ 𝑈 ↔ ¬ 𝑋 ∈ 𝑈 ) )
24 7 23 syl5ibrcom ⊢ ( 𝜑 → ( 𝑘 = 𝑋 → ¬ 𝑘 ∈ 𝑈 ) )
25 24 necon2ad ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑈 → 𝑘 ≠ 𝑋 ) )
26 25 imp ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝑘 ≠ 𝑋 )
27 pssdifn0 ⊢ ( ( 𝑘 ⊆ 𝑋 ∧ 𝑘 ≠ 𝑋 ) → ( 𝑋 ∖ 𝑘 ) ≠ ∅ )
28 21 26 27 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → ( 𝑋 ∖ 𝑘 ) ≠ ∅ )
29 eqid ⊢ ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) ) = ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) )
30 29 1 10 metdscn2 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑋 ∖ 𝑘 ) ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑘 ) ≠ ∅ ) → ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) )
31 15 16 28 30 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) )
32 10 14 6 31 fsumcn ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑈 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) )
33 8 32 eqeltrid ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) )
34 10 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
35 34 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
36 1 2 3 4 5 6 7 8 lebnumlem1 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ+ )
37 36 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ+ )
38 rpssre ⊢ ℝ+ ⊆ ℝ
39 37 38 sstrdi ⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ )
40 ax-resscn ⊢ ℝ ⊆ ℂ
41 40 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
42 cnrest2 ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ran 𝐹 ⊆ ℝ ∧ ℝ ⊆ ℂ ) → ( 𝐹 ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) ↔ 𝐹 ∈ ( 𝐽 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) )
43 35 39 41 42 syl3anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) ↔ 𝐹 ∈ ( 𝐽 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) )
44 33 43 mpbid ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) )
45 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
46 9 45 eqtri ⊢ 𝐾 = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
47 46 oveq2i ⊢ ( 𝐽 Cn 𝐾 ) = ( 𝐽 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
48 44 47 eleqtrrdi ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )