Metamath Proof Explorer

Theorem distgp

Description: Any group equipped with the discrete topology is a topological group. (Contributed by Mario Carneiro, 14-Aug-2015)

Ref Expression
Hypotheses distgp.1 ⊢ B = Base G
distgp.2 ⊢ J = TopOpen ⁡ G
Assertion distgp ⊢ G ∈ Grp ∧ J = 𝒫 B → G ∈ TopGrp

Proof

Step Hyp Ref Expression
1 distgp.1 ⊢ B = Base G
2 distgp.2 ⊢ J = TopOpen ⁡ G
3 simpl ⊢ G ∈ Grp ∧ J = 𝒫 B → G ∈ Grp
4 simpr ⊢ G ∈ Grp ∧ J = 𝒫 B → J = 𝒫 B
5 1 fvexi ⊢ B ∈ V
6 distopon ⊢ B ∈ V → 𝒫 B ∈ TopOn ⁡ B
7 5 6 ax-mp ⊢ 𝒫 B ∈ TopOn ⁡ B
8 4 7 eqeltrdi ⊢ G ∈ Grp ∧ J = 𝒫 B → J ∈ TopOn ⁡ B
9 1 2 istps ⊢ G ∈ TopSp ↔ J ∈ TopOn ⁡ B
10 8 9 sylibr ⊢ G ∈ Grp ∧ J = 𝒫 B → G ∈ TopSp
11 eqid ⊢ - G = - G
12 1 11 grpsubf ⊢ G ∈ Grp → - G : B × B ⟶ B
13 12 adantr ⊢ G ∈ Grp ∧ J = 𝒫 B → - G : B × B ⟶ B
14 5 5 xpex ⊢ B × B ∈ V
15 5 14 elmap ⊢ - G ∈ B B × B ↔ - G : B × B ⟶ B
16 13 15 sylibr ⊢ G ∈ Grp ∧ J = 𝒫 B → - G ∈ B B × B
17 4 4 oveq12d ⊢ G ∈ Grp ∧ J = 𝒫 B → J × t J = 𝒫 B × t 𝒫 B
18 txdis ⊢ B ∈ V ∧ B ∈ V → 𝒫 B × t 𝒫 B = 𝒫 B × B
19 5 5 18 mp2an ⊢ 𝒫 B × t 𝒫 B = 𝒫 B × B
20 17 19 eqtrdi ⊢ G ∈ Grp ∧ J = 𝒫 B → J × t J = 𝒫 B × B
21 20 oveq1d ⊢ G ∈ Grp ∧ J = 𝒫 B → J × t J Cn J = 𝒫 B × B Cn J
22 cndis ⊢ B × B ∈ V ∧ J ∈ TopOn ⁡ B → 𝒫 B × B Cn J = B B × B
23 14 8 22 sylancr ⊢ G ∈ Grp ∧ J = 𝒫 B → 𝒫 B × B Cn J = B B × B
24 21 23 eqtrd ⊢ G ∈ Grp ∧ J = 𝒫 B → J × t J Cn J = B B × B
25 16 24 eleqtrrd ⊢ G ∈ Grp ∧ J = 𝒫 B → - G ∈ J × t J Cn J
26 2 11 istgp2 ⊢ G ∈ TopGrp ↔ G ∈ Grp ∧ G ∈ TopSp ∧ - G ∈ J × t J Cn J
27 3 10 25 26 syl3anbrc ⊢ G ∈ Grp ∧ J = 𝒫 B → G ∈ TopGrp