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 )