Metamath Proof Explorer

Theorem indistgp

Description: Any group equipped with the indiscrete 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 indistgp ⊢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 indistopon ⊢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 oveq2d ⊢G∈Grp∧J=∅B→J×tJCnJ=J×tJCn∅B
18 txtopon ⊢J∈TopOn⁡B∧J∈TopOn⁡B→J×tJ∈TopOn⁡B×B
19 8 8 18 syl2anc ⊢G∈Grp∧J=∅B→J×tJ∈TopOn⁡B×B
20 cnindis ⊢J×tJ∈TopOn⁡B×B∧B∈V→J×tJCn∅B=BB×B
21 19 5 20 sylancl ⊢G∈Grp∧J=∅B→J×tJCn∅B=BB×B
22 17 21 eqtrd ⊢G∈Grp∧J=∅B→J×tJCnJ=BB×B
23 16 22 eleqtrrd ⊢G∈Grp∧J=∅B→-G∈J×tJCnJ
24 2 11 istgp2 ⊢G∈TopGrp↔G∈Grp∧G∈TopSp∧-G∈J×tJCnJ
25 3 10 23 24 syl3anbrc ⊢G∈Grp∧J=∅B→G∈TopGrp