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 = Base G
distgp.2 J = TopOpen G
Assertion indistgp 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 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 B B × B - G : B × B B
16 13 15 sylibr G Grp J = B - G B B × B
17 4 oveq2d G Grp J = B J × t J Cn J = J × t J Cn B
18 txtopon J TopOn B J TopOn B J × t J TopOn B × B
19 8 8 18 syl2anc G Grp J = B J × t J TopOn B × B
20 cnindis J × t J TopOn B × B B V J × t J Cn B = B B × B
21 19 5 20 sylancl G Grp J = B J × t J Cn B = B B × B
22 17 21 eqtrd G Grp J = B J × t J Cn J = B B × B
23 16 22 eleqtrrd G Grp J = B - G J × t J Cn J
24 2 11 istgp2 G TopGrp G Grp G TopSp - G J × t J Cn J
25 3 10 23 24 syl3anbrc G Grp J = B G TopGrp