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 𝐵 = ( Base ‘ 𝐺 )
distgp.2 𝐽 = ( TopOpen ‘ 𝐺 )
Assertion distgp ( ( 𝐺 ∈ Grp ∧ 𝐽 = 𝒫 𝐵 ) → 𝐺 ∈ TopGrp )

Proof

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 )