Metamath Proof Explorer

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 ⊢ B = Base G
tgptsmscls.j ⊢ J = TopOpen ⁡ G
tgptsmscls.1 ⊢ φ → G ∈ CMnd
tgptsmscls.2 ⊢ φ → G ∈ TopGrp
tgptsmscls.a ⊢ φ → A ∈ V
tgptsmscls.f ⊢ φ → F : A ⟶ B
Assertion tgptsmscld ⊢ φ → G tsums F ∈ Clsd ⁡ J

Proof

Step Hyp Ref Expression
1 tgptsmscls.b ⊢ B = Base G
2 tgptsmscls.j ⊢ J = TopOpen ⁡ G
3 tgptsmscls.1 ⊢ φ → G ∈ CMnd
4 tgptsmscls.2 ⊢ φ → G ∈ TopGrp
5 tgptsmscls.a ⊢ φ → A ∈ V
6 tgptsmscls.f ⊢ φ → F : A ⟶ B
7 2 1 tgptopon ⊢ G ∈ TopGrp → J ∈ TopOn ⁡ B
8 4 7 syl ⊢ φ → J ∈ TopOn ⁡ B
9 topontop ⊢ J ∈ TopOn ⁡ B → J ∈ Top
10 8 9 syl ⊢ φ → J ∈ Top
11 0cld ⊢ J ∈ Top → ∅ ∈ Clsd ⁡ J
12 10 11 syl ⊢ φ → ∅ ∈ Clsd ⁡ J
13 eleq1 ⊢ G tsums F = ∅ → G tsums F ∈ Clsd ⁡ J ↔ ∅ ∈ Clsd ⁡ J
14 12 13 syl5ibrcom ⊢ φ → G tsums F = ∅ → G tsums F ∈ Clsd ⁡ J
15 n0 ⊢ G tsums F ≠ ∅ ↔ ∃ x x ∈ G tsums F
16 3 adantr ⊢ φ ∧ x ∈ G tsums F → G ∈ CMnd
17 4 adantr ⊢ φ ∧ x ∈ G tsums F → G ∈ TopGrp
18 5 adantr ⊢ φ ∧ x ∈ G tsums F → A ∈ V
19 6 adantr ⊢ φ ∧ x ∈ G tsums F → F : A ⟶ B
20 simpr ⊢ φ ∧ x ∈ G tsums F → x ∈ G tsums F
21 1 2 16 17 18 19 20 tgptsmscls ⊢ φ ∧ x ∈ G tsums F → G tsums F = cls ⁡ J ⁡ x
22 tgptps ⊢ G ∈ TopGrp → G ∈ TopSp
23 4 22 syl ⊢ φ → G ∈ TopSp
24 1 3 23 5 6 tsmscl ⊢ φ → G tsums F ⊆ B
25 toponuni ⊢ J ∈ TopOn ⁡ B → B = ⋃ J
26 8 25 syl ⊢ φ → B = ⋃ J
27 24 26 sseqtrd ⊢ φ → G tsums F ⊆ ⋃ J
28 27 sselda ⊢ φ ∧ x ∈ G tsums F → x ∈ ⋃ J
29 28 snssd ⊢ φ ∧ x ∈ G tsums F → x ⊆ ⋃ J
30 eqid ⊢ ⋃ J = ⋃ J
31 30 clscld ⊢ J ∈ Top ∧ x ⊆ ⋃ J → cls ⁡ J ⁡ x ∈ Clsd ⁡ J
32 10 29 31 syl2an2r ⊢ φ ∧ x ∈ G tsums F → cls ⁡ J ⁡ x ∈ Clsd ⁡ J
33 21 32 eqeltrd ⊢ φ ∧ x ∈ G tsums F → G tsums F ∈ Clsd ⁡ J
34 33 ex ⊢ φ → x ∈ G tsums F → G tsums F ∈ Clsd ⁡ J
35 34 exlimdv ⊢ φ → ∃ x x ∈ G tsums F → G tsums F ∈ Clsd ⁡ J
36 15 35 syl5bi ⊢ φ → G tsums F ≠ ∅ → G tsums F ∈ Clsd ⁡ J
37 14 36 pm2.61dne ⊢ φ → G tsums F ∈ Clsd ⁡ J