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	$⊢ C = {abs}^{-1} [\{1\}]$
	circgrp.2	$⊢ T = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} C$
Assertion	circgrp	$⊢ T \in Abel$

Proof

Step	Hyp	Ref	Expression
1		circgrp.1	$⊢ C = {abs}^{-1} [\{1\}]$
2		circgrp.2	$⊢ T = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} C$
3		oveq2	$⊢ x = y \to i x = i y$
4	3	fveq2d	$⊢ x = y \to e^{i x} = e^{i y}$
5	4	cbvmptv	$⊢ (x \in ℝ ⟼ e^{i x}) = (y \in ℝ ⟼ e^{i y})$
6	5 1	efifo	$⊢ (x \in ℝ ⟼ e^{i x}) : ℝ \underset{onto}{⟶} C$
7		forn	$⊢ (x \in ℝ ⟼ e^{i x}) : ℝ \underset{onto}{⟶} C \to ran (x \in ℝ ⟼ e^{i x}) = C$
8	6 7	ax-mp	$⊢ ran (x \in ℝ ⟼ e^{i x}) = C$
9	8	eqcomi	$⊢ C = ran (x \in ℝ ⟼ e^{i x})$
10	9	oveq2i	$⊢ {mulGrp}_{ℂ_{fld}} ↾_{𝑠} C = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} ran (x \in ℝ ⟼ e^{i x})$
11	2 10	eqtri	$⊢ T = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} ran (x \in ℝ ⟼ e^{i x})$
12		ax-icn	$⊢ i \in ℂ$
13	12	a1i	$⊢ ⊤ \to i \in ℂ$
14		resubdrg	$⊢ (ℝ \in SubRing (ℂ_{fld}) \land ℝ_{fld} \in DivRing)$
15	14	simpli	$⊢ ℝ \in SubRing (ℂ_{fld})$
16		subrgsubg	$⊢ ℝ \in SubRing (ℂ_{fld}) \to ℝ \in SubGrp (ℂ_{fld})$
17	15 16	ax-mp	$⊢ ℝ \in SubGrp (ℂ_{fld})$
18	17	a1i	$⊢ ⊤ \to ℝ \in SubGrp (ℂ_{fld})$
19	5 11 13 18	efabl	$⊢ ⊤ \to T \in Abel$
20	19	mptru	$⊢ T \in Abel$

Metamath Proof Explorer

Theorem circgrp

Proof