Theorem circgrp

Description: The circle group T is an Abelian group. (Contributed by Paul Chapman, 25-Mar-2008) (Revised by Mario Carneiro, 13-May-2014) (Revised by Thierry Arnoux, 26-Jan-2020)

	Ref	Expression
Hypotheses	circgrp.1	⊢ 𝐶 = ( ◡ abs “ { 1 } )
	circgrp.2	⊢ 𝑇 = ( ( mulGrp ‘ ℂfld ) ↾s 𝐶 )
Assertion	circgrp	⊢ 𝑇 ∈ Abel

Proof

Step	Hyp	Ref	Expression
1		circgrp.1	⊢ 𝐶 = ( ◡ abs “ { 1 } )
2		circgrp.2	⊢ 𝑇 = ( ( mulGrp ‘ ℂfld ) ↾s 𝐶 )
3		oveq2	⊢ ( 𝑥 = 𝑦 → ( i · 𝑥 ) = ( i · 𝑦 ) )
4	3	fveq2d	⊢ ( 𝑥 = 𝑦 → ( exp ‘ ( i · 𝑥 ) ) = ( exp ‘ ( i · 𝑦 ) ) )
5	4	cbvmptv	⊢ ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( i · 𝑥 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( exp ‘ ( i · 𝑦 ) ) )
6	5 1	efifo	⊢ ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( i · 𝑥 ) ) ) : ℝ –onto→ 𝐶
7		forn	⊢ ( ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( i · 𝑥 ) ) ) : ℝ –onto→ 𝐶 → ran ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( i · 𝑥 ) ) ) = 𝐶 )
8	6 7	ax-mp	⊢ ran ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( i · 𝑥 ) ) ) = 𝐶
9	8	eqcomi	⊢ 𝐶 = ran ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( i · 𝑥 ) ) )
10	9	oveq2i	⊢ ( ( mulGrp ‘ ℂfld ) ↾s 𝐶 ) = ( ( mulGrp ‘ ℂfld ) ↾s ran ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( i · 𝑥 ) ) ) )
11	2 10	eqtri	⊢ 𝑇 = ( ( mulGrp ‘ ℂfld ) ↾s ran ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( i · 𝑥 ) ) ) )
12		ax-icn	⊢ i ∈ ℂ
13	12	a1i	⊢ ( ⊤ → i ∈ ℂ )
14		resubdrg	⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) ∧ ℝfld ∈ DivRing )
15	14	simpli	⊢ ℝ ∈ ( SubRing ‘ ℂfld )
16		subrgsubg	⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) → ℝ ∈ ( SubGrp ‘ ℂfld ) )
17	15 16	ax-mp	⊢ ℝ ∈ ( SubGrp ‘ ℂfld )
18	17	a1i	⊢ ( ⊤ → ℝ ∈ ( SubGrp ‘ ℂfld ) )
19	5 11 13 18	efabl	⊢ ( ⊤ → 𝑇 ∈ Abel )
20	19	mptru	⊢ 𝑇 ∈ Abel