Metamath Proof Explorer

Theorem haustsms

Description: In a Hausdorff topological group, a sum has at most one limit point. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses tsmscl.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
tsmscl.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
tsmscl.2 ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
tsmscl.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
tsmscl.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
haustsms.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
haustsms.h ⊢ ( 𝜑 → 𝐽 ∈ Haus )
Assertion haustsms ( 𝜑 → ∃* 𝑥 𝑥 ∈ ( 𝐺 tsums 𝐹 ) )

Proof

Step Hyp Ref Expression
1 tsmscl.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 tsmscl.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
3 tsmscl.2 ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
4 tsmscl.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5 tsmscl.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
6 haustsms.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
7 haustsms.h ⊢ ( 𝜑 → 𝐽 ∈ Haus )
8 eqid ⊢ ( 𝒫 𝐴 ∩ Fin ) = ( 𝒫 𝐴 ∩ Fin )
9 eqid ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) = ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } )
10 eqid ⊢ ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) = ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } )
11 8 9 10 4 tsmsfbas ⊢ ( 𝜑 → ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ∈ ( fBas ‘ ( 𝒫 𝐴 ∩ Fin ) ) )
12 fgcl ⊢ ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ∈ ( fBas ‘ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ∈ ( Fil ‘ ( 𝒫 𝐴 ∩ Fin ) ) )
13 11 12 syl ⊢ ( 𝜑 → ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ∈ ( Fil ‘ ( 𝒫 𝐴 ∩ Fin ) ) )
14 1 8 2 4 5 tsmslem1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝐵 )
15 1 6 tpsuni ⊢ ( 𝐺 ∈ TopSp → 𝐵 = ∪ 𝐽 )
16 3 15 syl ⊢ ( 𝜑 → 𝐵 = ∪ 𝐽 )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐵 = ∪ 𝐽 )
18 14 17 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ ∪ 𝐽 )
19 18 fmpttd ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) : ( 𝒫 𝐴 ∩ Fin ) ⟶ ∪ 𝐽 )
20 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
21 20 hausflf ⊢ ( ( 𝐽 ∈ Haus ∧ ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ∈ ( Fil ‘ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) : ( 𝒫 𝐴 ∩ Fin ) ⟶ ∪ 𝐽 ) → ∃* 𝑥 𝑥 ∈ ( ( 𝐽 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) ) )
22 7 13 19 21 syl3anc ⊢ ( 𝜑 → ∃* 𝑥 𝑥 ∈ ( ( 𝐽 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) ) )
23 1 6 8 10 2 4 5 tsmsval ⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( ( 𝐽 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) ) )
24 23 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ↔ 𝑥 ∈ ( ( 𝐽 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) ) ) )
25 24 mobidv ⊢ ( 𝜑 → ( ∃* 𝑥 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ↔ ∃* 𝑥 𝑥 ∈ ( ( 𝐽 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) ) ) )
26 22 25 mpbird ⊢ ( 𝜑 → ∃* 𝑥 𝑥 ∈ ( 𝐺 tsums 𝐹 ) )