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 = ( RRfld /s ( RRfld ~QG ZZ ) )
Assertion rzgrp 
|- R e. Grp

Proof

Step Hyp Ref Expression
1 rzgrp.r 
 |-  R = ( RRfld /s ( RRfld ~QG ZZ ) )
2 zsubrg 
 |-  ZZ e. ( SubRing ` CCfld )
3 zssre 
 |-  ZZ C_ RR
4 resubdrg 
 |-  ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )
5 4 simpli 
 |-  RR e. ( SubRing ` CCfld )
6 df-refld 
 |-  RRfld = ( CCfld |`s RR )
7 6 subsubrg 
 |-  ( RR e. ( SubRing ` CCfld ) -> ( ZZ e. ( SubRing ` RRfld ) <-> ( ZZ e. ( SubRing ` CCfld ) /\ ZZ C_ RR ) ) )
8 5 7 ax-mp 
 |-  ( ZZ e. ( SubRing ` RRfld ) <-> ( ZZ e. ( SubRing ` CCfld ) /\ ZZ C_ RR ) )
9 2 3 8 mpbir2an 
 |-  ZZ e. ( SubRing ` RRfld )
10 subrgsubg 
 |-  ( ZZ e. ( SubRing ` RRfld ) -> ZZ e. ( SubGrp ` RRfld ) )
11 9 10 ax-mp 
 |-  ZZ e. ( SubGrp ` RRfld )
12 simpl 
 |-  ( ( x e. RR /\ y e. RR ) -> x e. RR )
13 12 recnd 
 |-  ( ( x e. RR /\ y e. RR ) -> x e. CC )
14 simpr 
 |-  ( ( x e. RR /\ y e. RR ) -> y e. RR )
15 14 recnd 
 |-  ( ( x e. RR /\ y e. RR ) -> y e. CC )
16 13 15 addcomd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + y ) = ( y + x ) )
17 16 eleq1d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( x + y ) e. ZZ <-> ( y + x ) e. ZZ ) )
18 17 rgen2 
 |-  A. x e. RR A. y e. RR ( ( x + y ) e. ZZ <-> ( y + x ) e. ZZ )
19 rebase 
 |-  RR = ( Base ` RRfld )
20 replusg 
 |-  + = ( +g ` RRfld )
21 19 20 isnsg 
 |-  ( ZZ e. ( NrmSGrp ` RRfld ) <-> ( ZZ e. ( SubGrp ` RRfld ) /\ A. x e. RR A. y e. RR ( ( x + y ) e. ZZ <-> ( y + x ) e. ZZ ) ) )
22 11 18 21 mpbir2an 
 |-  ZZ e. ( NrmSGrp ` RRfld )
23 1 qusgrp 
 |-  ( ZZ e. ( NrmSGrp ` RRfld ) -> R e. Grp )
24 22 23 ax-mp 
 |-  R e. Grp