Step |
Hyp |
Ref |
Expression |
1 |
|
distgp.1 |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
distgp.2 |
⊢ 𝐽 = ( TopOpen ‘ 𝐺 ) |
3 |
|
simpl |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐽 = 𝒫 𝐵 ) → 𝐺 ∈ Grp ) |
4 |
|
simpr |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐽 = 𝒫 𝐵 ) → 𝐽 = 𝒫 𝐵 ) |
5 |
1
|
fvexi |
⊢ 𝐵 ∈ V |
6 |
|
distopon |
⊢ ( 𝐵 ∈ V → 𝒫 𝐵 ∈ ( TopOn ‘ 𝐵 ) ) |
7 |
5 6
|
ax-mp |
⊢ 𝒫 𝐵 ∈ ( TopOn ‘ 𝐵 ) |
8 |
4 7
|
eqeltrdi |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐽 = 𝒫 𝐵 ) → 𝐽 ∈ ( TopOn ‘ 𝐵 ) ) |
9 |
1 2
|
istps |
⊢ ( 𝐺 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ 𝐵 ) ) |
10 |
8 9
|
sylibr |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐽 = 𝒫 𝐵 ) → 𝐺 ∈ TopSp ) |
11 |
|
eqid |
⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 ) |
12 |
1 11
|
grpsubf |
⊢ ( 𝐺 ∈ Grp → ( -g ‘ 𝐺 ) : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ) |
13 |
12
|
adantr |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐽 = 𝒫 𝐵 ) → ( -g ‘ 𝐺 ) : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ) |
14 |
5 5
|
xpex |
⊢ ( 𝐵 × 𝐵 ) ∈ V |
15 |
5 14
|
elmap |
⊢ ( ( -g ‘ 𝐺 ) ∈ ( 𝐵 ↑m ( 𝐵 × 𝐵 ) ) ↔ ( -g ‘ 𝐺 ) : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ) |
16 |
13 15
|
sylibr |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐽 = 𝒫 𝐵 ) → ( -g ‘ 𝐺 ) ∈ ( 𝐵 ↑m ( 𝐵 × 𝐵 ) ) ) |
17 |
4 4
|
oveq12d |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐽 = 𝒫 𝐵 ) → ( 𝐽 ×t 𝐽 ) = ( 𝒫 𝐵 ×t 𝒫 𝐵 ) ) |
18 |
|
txdis |
⊢ ( ( 𝐵 ∈ V ∧ 𝐵 ∈ V ) → ( 𝒫 𝐵 ×t 𝒫 𝐵 ) = 𝒫 ( 𝐵 × 𝐵 ) ) |
19 |
5 5 18
|
mp2an |
⊢ ( 𝒫 𝐵 ×t 𝒫 𝐵 ) = 𝒫 ( 𝐵 × 𝐵 ) |
20 |
17 19
|
eqtrdi |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐽 = 𝒫 𝐵 ) → ( 𝐽 ×t 𝐽 ) = 𝒫 ( 𝐵 × 𝐵 ) ) |
21 |
20
|
oveq1d |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐽 = 𝒫 𝐵 ) → ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) = ( 𝒫 ( 𝐵 × 𝐵 ) Cn 𝐽 ) ) |
22 |
|
cndis |
⊢ ( ( ( 𝐵 × 𝐵 ) ∈ V ∧ 𝐽 ∈ ( TopOn ‘ 𝐵 ) ) → ( 𝒫 ( 𝐵 × 𝐵 ) Cn 𝐽 ) = ( 𝐵 ↑m ( 𝐵 × 𝐵 ) ) ) |
23 |
14 8 22
|
sylancr |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐽 = 𝒫 𝐵 ) → ( 𝒫 ( 𝐵 × 𝐵 ) Cn 𝐽 ) = ( 𝐵 ↑m ( 𝐵 × 𝐵 ) ) ) |
24 |
21 23
|
eqtrd |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐽 = 𝒫 𝐵 ) → ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) = ( 𝐵 ↑m ( 𝐵 × 𝐵 ) ) ) |
25 |
16 24
|
eleqtrrd |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐽 = 𝒫 𝐵 ) → ( -g ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) |
26 |
2 11
|
istgp2 |
⊢ ( 𝐺 ∈ TopGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ ( -g ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) ) |
27 |
3 10 25 26
|
syl3anbrc |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐽 = 𝒫 𝐵 ) → 𝐺 ∈ TopGrp ) |