Metamath Proof Explorer

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 ⊢ C = abs -1 1
circgrp.2 ⊢ T = mulGrp ℂ fld ↾ 𝑠 C
Assertion circgrp ⊢ T ∈ Abel

Proof

Step Hyp Ref Expression
1 circgrp.1 ⊢ C = abs -1 1
2 circgrp.2 ⊢ T = mulGrp ℂ fld ↾ 𝑠 C
3 oveq2 ⊢ x = y → i ⁢ x = i ⁢ y
4 3 fveq2d ⊢ x = y → e i ⁢ x = e i ⁢ y
5 4 cbvmptv ⊢ x ∈ ℝ ⟼ e i ⁢ x = y ∈ ℝ ⟼ e i ⁢ y
6 5 1 efifo ⊢ x ∈ ℝ ⟼ e i ⁢ x : ℝ ⟶ onto C
7 forn ⊢ x ∈ ℝ ⟼ e i ⁢ x : ℝ ⟶ onto C → ran ⁡ x ∈ ℝ ⟼ e i ⁢ x = C
8 6 7 ax-mp ⊢ ran ⁡ x ∈ ℝ ⟼ e i ⁢ x = C
9 8 eqcomi ⊢ C = ran ⁡ x ∈ ℝ ⟼ e i ⁢ x
10 9 oveq2i ⊢ mulGrp ℂ fld ↾ 𝑠 C = mulGrp ℂ fld ↾ 𝑠 ran ⁡ x ∈ ℝ ⟼ e i ⁢ x
11 2 10 eqtri ⊢ T = mulGrp ℂ fld ↾ 𝑠 ran ⁡ x ∈ ℝ ⟼ e i ⁢ x
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 ⊢ ⊤ → T ∈ Abel
20 19 mptru ⊢ T ∈ Abel