This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑅 = ( ℝfld /s ( ℝfld ~QG ℤ ) )
Assertion rzgrp 𝑅 ∈ Grp

Proof

Step Hyp Ref Expression
1 rzgrp.r ⊢ 𝑅 = ( ℝfld /s ( ℝfld ~QG ℤ ) )
2 zsubrg ⊢ ℤ ∈ ( SubRing ‘ ℂfld )
3 zssre ⊢ ℤ ⊆ ℝ
4 resubdrg ⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) ∧ ℝfld ∈ DivRing )
5 4 simpli ⊢ ℝ ∈ ( SubRing ‘ ℂfld )
6 df-refld ⊢ ℝfld = ( ℂfld ↾s ℝ )
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 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑥 ∈ ℝ )
13 12 recnd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑥 ∈ ℂ )
14 simpr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
15 14 recnd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
16 13 15 addcomd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
17 16 eleq1d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 + 𝑦 ) ∈ ℤ ↔ ( 𝑦 + 𝑥 ) ∈ ℤ ) )
18 17 rgen2 ⊢ ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ( ( 𝑥 + 𝑦 ) ∈ ℤ ↔ ( 𝑦 + 𝑥 ) ∈ ℤ )
19 rebase ⊢ ℝ = ( Base ‘ ℝfld )
20 replusg ⊢ + = ( +g ‘ ℝfld )
21 19 20 isnsg ⊢ ( ℤ ∈ ( NrmSGrp ‘ ℝfld ) ↔ ( ℤ ∈ ( SubGrp ‘ ℝfld ) ∧ ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ( ( 𝑥 + 𝑦 ) ∈ ℤ ↔ ( 𝑦 + 𝑥 ) ∈ ℤ ) ) )
22 11 18 21 mpbir2an ⊢ ℤ ∈ ( NrmSGrp ‘ ℝfld )
23 1 qusgrp ⊢ ( ℤ ∈ ( NrmSGrp ‘ ℝfld ) → 𝑅 ∈ Grp )
24 22 23 ax-mp ⊢ 𝑅 ∈ Grp