This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem indistgp

Description: Any group equipped with the indiscrete topology is a topological group. (Contributed by Mario Carneiro, 14-Aug-2015)

Ref Expression
Hypotheses distgp.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
distgp.2 ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
Assertion indistgp ( ( 𝐺 ∈ 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 indistopon ⊢ ( 𝐵 ∈ 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 oveq2d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐽 = { ∅ , 𝐵 } ) → ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) = ( ( 𝐽 ×t 𝐽 ) Cn { ∅ , 𝐵 } ) )
18 txtopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ∧ 𝐽 ∈ ( TopOn ‘ 𝐵 ) ) → ( 𝐽 ×t 𝐽 ) ∈ ( TopOn ‘ ( 𝐵 × 𝐵 ) ) )
19 8 8 18 syl2anc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐽 = { ∅ , 𝐵 } ) → ( 𝐽 ×t 𝐽 ) ∈ ( TopOn ‘ ( 𝐵 × 𝐵 ) ) )
20 cnindis ⊢ ( ( ( 𝐽 ×t 𝐽 ) ∈ ( TopOn ‘ ( 𝐵 × 𝐵 ) ) ∧ 𝐵 ∈ V ) → ( ( 𝐽 ×t 𝐽 ) Cn { ∅ , 𝐵 } ) = ( 𝐵 ↑m ( 𝐵 × 𝐵 ) ) )
21 19 5 20 sylancl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐽 = { ∅ , 𝐵 } ) → ( ( 𝐽 ×t 𝐽 ) Cn { ∅ , 𝐵 } ) = ( 𝐵 ↑m ( 𝐵 × 𝐵 ) ) )
22 17 21 eqtrd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐽 = { ∅ , 𝐵 } ) → ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) = ( 𝐵 ↑m ( 𝐵 × 𝐵 ) ) )
23 16 22 eleqtrrd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐽 = { ∅ , 𝐵 } ) → ( -g ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
24 2 11 istgp2 ⊢ ( 𝐺 ∈ TopGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ ( -g ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) )
25 3 10 23 24 syl3anbrc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐽 = { ∅ , 𝐵 } ) → 𝐺 ∈ TopGrp )