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 e. Grp /\ J = { (/) , 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 = { (/) , B } ) -> G e. Grp )
4 simpr
 |-  ( ( G e. Grp /\ J = { (/) , B } ) -> J = { (/) , B } )
5 1 fvexi
 |-  B e. _V
6 indistopon
 |-  ( B e. _V -> { (/) , B } e. ( TopOn ` B ) )
7 5 6 ax-mp
 |-  { (/) , B } e. ( TopOn ` B )
8 4 7 eqeltrdi
 |-  ( ( G e. Grp /\ J = { (/) , B } ) -> J e. ( TopOn ` B ) )
9 1 2 istps
 |-  ( G e. TopSp <-> J e. ( TopOn ` B ) )
10 8 9 sylibr
 |-  ( ( G e. Grp /\ J = { (/) , 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 = { (/) , 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 = { (/) , B } ) -> ( -g ` G ) e. ( B ^m ( B X. B ) ) )
17 4 oveq2d
 |-  ( ( G e. Grp /\ J = { (/) , B } ) -> ( ( J tX J ) Cn J ) = ( ( J tX J ) Cn { (/) , B } ) )
18 txtopon
 |-  ( ( J e. ( TopOn ` B ) /\ J e. ( TopOn ` B ) ) -> ( J tX J ) e. ( TopOn ` ( B X. B ) ) )
19 8 8 18 syl2anc
 |-  ( ( G e. Grp /\ J = { (/) , B } ) -> ( J tX J ) e. ( TopOn ` ( B X. B ) ) )
20 cnindis
 |-  ( ( ( J tX J ) e. ( TopOn ` ( B X. B ) ) /\ B e. _V ) -> ( ( J tX J ) Cn { (/) , B } ) = ( B ^m ( B X. B ) ) )
21 19 5 20 sylancl
 |-  ( ( G e. Grp /\ J = { (/) , B } ) -> ( ( J tX J ) Cn { (/) , B } ) = ( B ^m ( B X. B ) ) )
22 17 21 eqtrd
 |-  ( ( G e. Grp /\ J = { (/) , B } ) -> ( ( J tX J ) Cn J ) = ( B ^m ( B X. B ) ) )
23 16 22 eleqtrrd
 |-  ( ( G e. Grp /\ J = { (/) , B } ) -> ( -g ` G ) e. ( ( J tX J ) Cn J ) )
24 2 11 istgp2
 |-  ( G e. TopGrp <-> ( G e. Grp /\ G e. TopSp /\ ( -g ` G ) e. ( ( J tX J ) Cn J ) ) )
25 3 10 23 24 syl3anbrc
 |-  ( ( G e. Grp /\ J = { (/) , B } ) -> G e. TopGrp )