Theorem tgptsmscld

Description: The set of limit points to an infinite sum in a topological group is closed. (Contributed by Mario Carneiro, 22-Sep-2015)

	Ref	Expression
Hypotheses	tgptsmscls.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	tgptsmscls.j	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
	tgptsmscls.1	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	tgptsmscls.2	⊢ ( 𝜑 → 𝐺 ∈ TopGrp )
	tgptsmscls.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	tgptsmscls.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
Assertion	tgptsmscld	⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		tgptsmscls.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		tgptsmscls.j	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
3		tgptsmscls.1	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4		tgptsmscls.2	⊢ ( 𝜑 → 𝐺 ∈ TopGrp )
5		tgptsmscls.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6		tgptsmscls.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7	2 1	tgptopon	⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
8	4 7	syl	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
9		topontop	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → 𝐽 ∈ Top )
10	8 9	syl	⊢ ( 𝜑 → 𝐽 ∈ Top )
11		0cld	⊢ ( 𝐽 ∈ Top → ∅ ∈ ( Clsd ‘ 𝐽 ) )
12	10 11	syl	⊢ ( 𝜑 → ∅ ∈ ( Clsd ‘ 𝐽 ) )
13		eleq1	⊢ ( ( 𝐺 tsums 𝐹 ) = ∅ → ( ( 𝐺 tsums 𝐹 ) ∈ ( Clsd ‘ 𝐽 ) ↔ ∅ ∈ ( Clsd ‘ 𝐽 ) ) )
14	12 13	syl5ibrcom	⊢ ( 𝜑 → ( ( 𝐺 tsums 𝐹 ) = ∅ → ( 𝐺 tsums 𝐹 ) ∈ ( Clsd ‘ 𝐽 ) ) )
15		n0	⊢ ( ( 𝐺 tsums 𝐹 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝐺 tsums 𝐹 ) )
16	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ) → 𝐺 ∈ CMnd )
17	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ) → 𝐺 ∈ TopGrp )
18	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ) → 𝐴 ∈ 𝑉 )
19	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
20		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ) → 𝑥 ∈ ( 𝐺 tsums 𝐹 ) )
21	1 2 16 17 18 19 20	tgptsmscls	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ) → ( 𝐺 tsums 𝐹 ) = ( ( cls ‘ 𝐽 ) ‘ { 𝑥 } ) )
22		tgptps	⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopSp )
23	4 22	syl	⊢ ( 𝜑 → 𝐺 ∈ TopSp )
24	1 3 23 5 6	tsmscl	⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) ⊆ 𝐵 )
25		toponuni	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → 𝐵 = ∪ 𝐽 )
26	8 25	syl	⊢ ( 𝜑 → 𝐵 = ∪ 𝐽 )
27	24 26	sseqtrd	⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) ⊆ ∪ 𝐽 )
28	27	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ) → 𝑥 ∈ ∪ 𝐽 )
29	28	snssd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ) → { 𝑥 } ⊆ ∪ 𝐽 )
30		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
31	30	clscld	⊢ ( ( 𝐽 ∈ Top ∧ { 𝑥 } ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ { 𝑥 } ) ∈ ( Clsd ‘ 𝐽 ) )
32	10 29 31	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ) → ( ( cls ‘ 𝐽 ) ‘ { 𝑥 } ) ∈ ( Clsd ‘ 𝐽 ) )
33	21 32	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ) → ( 𝐺 tsums 𝐹 ) ∈ ( Clsd ‘ 𝐽 ) )
34	33	ex	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) → ( 𝐺 tsums 𝐹 ) ∈ ( Clsd ‘ 𝐽 ) ) )
35	34	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑥 𝑥 ∈ ( 𝐺 tsums 𝐹 ) → ( 𝐺 tsums 𝐹 ) ∈ ( Clsd ‘ 𝐽 ) ) )
36	15 35	syl5bi	⊢ ( 𝜑 → ( ( 𝐺 tsums 𝐹 ) ≠ ∅ → ( 𝐺 tsums 𝐹 ) ∈ ( Clsd ‘ 𝐽 ) ) )
37	14 36	pm2.61dne	⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) ∈ ( Clsd ‘ 𝐽 ) )