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	$⊢ B = {Base}_{G}$
	tsmscl.1	$⊢ φ \to G \in CMnd$
	tsmscl.2	$⊢ φ \to G \in TopSp$
	tsmscl.a	$⊢ φ \to A \in V$
	tsmscl.f	$⊢ φ \to F : A ⟶ B$
	haustsms.j	$⊢ J = TopOpen (G)$
	haustsms.h	$⊢ φ \to J \in Haus$
Assertion	haustsms	$⊢ φ \to \exists^{*} x x \in (G tsums F)$

Proof

Step	Hyp	Ref	Expression
1		tsmscl.b	$⊢ B = {Base}_{G}$
2		tsmscl.1	$⊢ φ \to G \in CMnd$
3		tsmscl.2	$⊢ φ \to G \in TopSp$
4		tsmscl.a	$⊢ φ \to A \in V$
5		tsmscl.f	$⊢ φ \to F : A ⟶ B$
6		haustsms.j	$⊢ J = TopOpen (G)$
7		haustsms.h	$⊢ φ \to J \in Haus$
8		eqid	$⊢ 𝒫 A \cap Fin = 𝒫 A \cap Fin$
9		eqid	$⊢ (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}) = (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\})$
10		eqid	$⊢ ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}) = ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\})$
11	8 9 10 4	tsmsfbas	$⊢ φ \to ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}) \in fBas (𝒫 A \cap Fin)$
12		fgcl	$⊢ ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}) \in fBas (𝒫 A \cap Fin) \to (𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}) \in Fil (𝒫 A \cap Fin)$
13	11 12	syl	$⊢ φ \to (𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}) \in Fil (𝒫 A \cap Fin)$
14	1 8 2 4 5	tsmslem1	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to \sum_{G} ({F ↾}_{z}) \in B$
15	1 6	tpsuni	$⊢ G \in TopSp \to B = ⋃ J$
16	3 15	syl	$⊢ φ \to B = ⋃ J$
17	16	adantr	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to B = ⋃ J$
18	14 17	eleqtrd	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to \sum_{G} ({F ↾}_{z}) \in ⋃ J$
19	18	fmpttd	$⊢ φ \to (z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{z})) : 𝒫 A \cap Fin ⟶ ⋃ J$
20		eqid	$⊢ ⋃ J = ⋃ J$
21	20	hausflf	$⊢ (J \in Haus \land (𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}) \in Fil (𝒫 A \cap Fin) \land (z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{z})) : 𝒫 A \cap Fin ⟶ ⋃ J) \to \exists^{*} x x \in (J fLimf ((𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}))) ((z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{z})))$
22	7 13 19 21	syl3anc	$⊢ φ \to \exists^{*} x x \in (J fLimf ((𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}))) ((z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{z})))$
23	1 6 8 10 2 4 5	tsmsval	$⊢ φ \to G tsums F = (J fLimf ((𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}))) ((z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{z})))$
24	23	eleq2d	$⊢ φ \to (x \in (G tsums F) \leftrightarrow x \in (J fLimf ((𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}))) ((z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{z}))))$
25	24	mobidv	$⊢ φ \to (\exists^{} x x \in (G tsums F) \leftrightarrow \exists^{} x x \in (J fLimf ((𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}))) ((z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{z}))))$
26	22 25	mpbird	$⊢ φ \to \exists^{*} x x \in (G tsums F)$

Metamath Proof Explorer

Theorem haustsms

Proof