Metamath Proof Explorer

Theorem rzgrp

Description: The quotient group RR / ZZ is a group. (Contributed by Thierry Arnoux, 26-Jan-2020)

Ref Expression
Hypothesis rzgrp.r ⊢ R = ℝ fld / 𝑠 ℝ fld ~ QG ℤ
Assertion rzgrp ⊢ R ∈ Grp

Proof

Step Hyp Ref Expression
1 rzgrp.r ⊢ R = ℝ fld / 𝑠 ℝ fld ~ QG ℤ
2 zsubrg ⊢ ℤ ∈ SubRing ⁡ ℂ fld
3 zssre ⊢ ℤ ⊆ ℝ
4 resubdrg ⊢ ℝ ∈ SubRing ⁡ ℂ fld ∧ ℝ fld ∈ DivRing
5 4 simpli ⊢ ℝ ∈ SubRing ⁡ ℂ fld
6 df-refld ⊢ ℝ fld = ℂ fld ↾ 𝑠 ℝ
7 6 subsubrg ⊢ ℝ ∈ SubRing ⁡ ℂ fld → ℤ ∈ SubRing ⁡ ℝ fld ↔ ℤ ∈ SubRing ⁡ ℂ fld ∧ ℤ ⊆ ℝ
8 5 7 ax-mp ⊢ ℤ ∈ SubRing ⁡ ℝ fld ↔ ℤ ∈ SubRing ⁡ ℂ fld ∧ ℤ ⊆ ℝ
9 2 3 8 mpbir2an ⊢ ℤ ∈ SubRing ⁡ ℝ fld
10 subrgsubg ⊢ ℤ ∈ SubRing ⁡ ℝ fld → ℤ ∈ SubGrp ⁡ ℝ fld
11 9 10 ax-mp ⊢ ℤ ∈ SubGrp ⁡ ℝ fld
12 simpl ⊢ x ∈ ℝ ∧ y ∈ ℝ → x ∈ ℝ
13 12 recnd ⊢ x ∈ ℝ ∧ y ∈ ℝ → x ∈ ℂ
14 simpr ⊢ x ∈ ℝ ∧ y ∈ ℝ → y ∈ ℝ
15 14 recnd ⊢ x ∈ ℝ ∧ y ∈ ℝ → y ∈ ℂ
16 13 15 addcomd ⊢ x ∈ ℝ ∧ y ∈ ℝ → x + y = y + x
17 16 eleq1d ⊢ x ∈ ℝ ∧ y ∈ ℝ → x + y ∈ ℤ ↔ y + x ∈ ℤ
18 17 rgen2 ⊢ ∀ x ∈ ℝ ∀ y ∈ ℝ x + y ∈ ℤ ↔ y + x ∈ ℤ
19 rebase ⊢ ℝ = Base ℝ fld
20 replusg ⊢ + = + ℝ fld
21 19 20 isnsg ⊢ ℤ ∈ NrmSGrp ⁡ ℝ fld ↔ ℤ ∈ SubGrp ⁡ ℝ fld ∧ ∀ x ∈ ℝ ∀ y ∈ ℝ x + y ∈ ℤ ↔ y + x ∈ ℤ
22 11 18 21 mpbir2an ⊢ ℤ ∈ NrmSGrp ⁡ ℝ fld
23 1 qusgrp ⊢ ℤ ∈ NrmSGrp ⁡ ℝ fld → R ∈ Grp
24 22 23 ax-mp ⊢ R ∈ Grp