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 )

Metamath Proof Explorer

Theorem distgp

Proof