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