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=BaseG
distgp.2 ⊢J=TopOpen⁡G
Assertion distgp ⊢G∈Grp∧J=𝒫B→G∈TopGrp

Proof

Step Hyp Ref Expression
1 distgp.1 ⊢B=BaseG
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∈BB×B↔-G:B×B⟶B
16 13 15 sylibr ⊢G∈Grp∧J=𝒫B→-G∈BB×B
17 4 4 oveq12d ⊢G∈Grp∧J=𝒫B→J×tJ=𝒫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×tJ=𝒫B×B
21 20 oveq1d ⊢G∈Grp∧J=𝒫B→J×tJCnJ=𝒫B×BCnJ
22 cndis ⊢B×B∈V∧J∈TopOn⁡B→𝒫B×BCnJ=BB×B
23 14 8 22 sylancr ⊢G∈Grp∧J=𝒫B→𝒫B×BCnJ=BB×B
24 21 23 eqtrd ⊢G∈Grp∧J=𝒫B→J×tJCnJ=BB×B
25 16 24 eleqtrrd ⊢G∈Grp∧J=𝒫B→-G∈J×tJCnJ
26 2 11 istgp2 ⊢G∈TopGrp↔G∈Grp∧G∈TopSp∧-G∈J×tJCnJ
27 3 10 25 26 syl3anbrc ⊢G∈Grp∧J=𝒫B→G∈TopGrp