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 ) |