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