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 )