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