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 e. Grp /\ J = ~P B ) -> G e. TopGrp )

Proof

Step Hyp Ref Expression
1 distgp.1 
 |-  B = ( Base ` G )
2 distgp.2 
 |-  J = ( TopOpen ` G )
3 simpl 
 |-  ( ( G e. Grp /\ J = ~P B ) -> G e. Grp )
4 simpr 
 |-  ( ( G e. Grp /\ J = ~P B ) -> J = ~P B )
5 1 fvexi 
 |-  B e. _V
6 distopon 
 |-  ( B e. _V -> ~P B e. ( TopOn ` B ) )
7 5 6 ax-mp 
 |-  ~P B e. ( TopOn ` B )
8 4 7 eqeltrdi 
 |-  ( ( G e. Grp /\ J = ~P B ) -> J e. ( TopOn ` B ) )
9 1 2 istps 
 |-  ( G e. TopSp <-> J e. ( TopOn ` B ) )
10 8 9 sylibr 
 |-  ( ( G e. Grp /\ J = ~P B ) -> G e. TopSp )
11 eqid 
 |-  ( -g ` G ) = ( -g ` G )
12 1 11 grpsubf 
 |-  ( G e. Grp -> ( -g ` G ) : ( B X. B ) --> B )
13 12 adantr 
 |-  ( ( G e. Grp /\ J = ~P B ) -> ( -g ` G ) : ( B X. B ) --> B )
14 5 5 xpex 
 |-  ( B X. B ) e. _V
15 5 14 elmap 
 |-  ( ( -g ` G ) e. ( B ^m ( B X. B ) ) <-> ( -g ` G ) : ( B X. B ) --> B )
16 13 15 sylibr 
 |-  ( ( G e. Grp /\ J = ~P B ) -> ( -g ` G ) e. ( B ^m ( B X. B ) ) )
17 4 4 oveq12d 
 |-  ( ( G e. Grp /\ J = ~P B ) -> ( J tX J ) = ( ~P B tX ~P B ) )
18 txdis 
 |-  ( ( B e. _V /\ B e. _V ) -> ( ~P B tX ~P B ) = ~P ( B X. B ) )
19 5 5 18 mp2an 
 |-  ( ~P B tX ~P B ) = ~P ( B X. B )
20 17 19 eqtrdi 
 |-  ( ( G e. Grp /\ J = ~P B ) -> ( J tX J ) = ~P ( B X. B ) )
21 20 oveq1d 
 |-  ( ( G e. Grp /\ J = ~P B ) -> ( ( J tX J ) Cn J ) = ( ~P ( B X. B ) Cn J ) )
22 cndis 
 |-  ( ( ( B X. B ) e. _V /\ J e. ( TopOn ` B ) ) -> ( ~P ( B X. B ) Cn J ) = ( B ^m ( B X. B ) ) )
23 14 8 22 sylancr 
 |-  ( ( G e. Grp /\ J = ~P B ) -> ( ~P ( B X. B ) Cn J ) = ( B ^m ( B X. B ) ) )
24 21 23 eqtrd 
 |-  ( ( G e. Grp /\ J = ~P B ) -> ( ( J tX J ) Cn J ) = ( B ^m ( B X. B ) ) )
25 16 24 eleqtrrd 
 |-  ( ( G e. Grp /\ J = ~P B ) -> ( -g ` G ) e. ( ( J tX J ) Cn J ) )
26 2 11 istgp2 
 |-  ( G e. TopGrp <-> ( G e. Grp /\ G e. TopSp /\ ( -g ` G ) e. ( ( J tX J ) Cn J ) ) )
27 3 10 25 26 syl3anbrc 
 |-  ( ( G e. Grp /\ J = ~P B ) -> G e. TopGrp )