Metamath Proof Explorer

Theorem zringcyg

Description: The integers are a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016) (Revised by AV, 9-Jun-2019)

Ref Expression
Assertion zringcyg 
|- ZZring e. CycGrp

Proof

Step Hyp Ref Expression
1 zringbas 
 |-  ZZ = ( Base ` ZZring )
2 eqid 
 |-  ( .g ` ZZring ) = ( .g ` ZZring )
3 zsubrg 
 |-  ZZ e. ( SubRing ` CCfld )
4 subrgsubg 
 |-  ( ZZ e. ( SubRing ` CCfld ) -> ZZ e. ( SubGrp ` CCfld ) )
5 3 4 ax-mp 
 |-  ZZ e. ( SubGrp ` CCfld )
6 df-zring 
 |-  ZZring = ( CCfld |`s ZZ )
7 6 subggrp 
 |-  ( ZZ e. ( SubGrp ` CCfld ) -> ZZring e. Grp )
8 5 7 mp1i 
 |-  ( T. -> ZZring e. Grp )
9 1zzd 
 |-  ( T. -> 1 e. ZZ )
10 ax-1cn 
 |-  1 e. CC
11 cnfldmulg 
 |-  ( ( x e. ZZ /\ 1 e. CC ) -> ( x ( .g ` CCfld ) 1 ) = ( x x. 1 ) )
12 10 11 mpan2 
 |-  ( x e. ZZ -> ( x ( .g ` CCfld ) 1 ) = ( x x. 1 ) )
13 1z 
 |-  1 e. ZZ
14 eqid 
 |-  ( .g ` CCfld ) = ( .g ` CCfld )
15 14 6 2 subgmulg 
 |-  ( ( ZZ e. ( SubGrp ` CCfld ) /\ x e. ZZ /\ 1 e. ZZ ) -> ( x ( .g ` CCfld ) 1 ) = ( x ( .g ` ZZring ) 1 ) )
16 5 13 15 mp3an13 
 |-  ( x e. ZZ -> ( x ( .g ` CCfld ) 1 ) = ( x ( .g ` ZZring ) 1 ) )
17 zcn 
 |-  ( x e. ZZ -> x e. CC )
18 17 mulid1d 
 |-  ( x e. ZZ -> ( x x. 1 ) = x )
19 12 16 18 3eqtr3rd 
 |-  ( x e. ZZ -> x = ( x ( .g ` ZZring ) 1 ) )
20 oveq1 
 |-  ( z = x -> ( z ( .g ` ZZring ) 1 ) = ( x ( .g ` ZZring ) 1 ) )
21 20 rspceeqv 
 |-  ( ( x e. ZZ /\ x = ( x ( .g ` ZZring ) 1 ) ) -> E. z e. ZZ x = ( z ( .g ` ZZring ) 1 ) )
22 19 21 mpdan 
 |-  ( x e. ZZ -> E. z e. ZZ x = ( z ( .g ` ZZring ) 1 ) )
23 22 adantl 
 |-  ( ( T. /\ x e. ZZ ) -> E. z e. ZZ x = ( z ( .g ` ZZring ) 1 ) )
24 1 2 8 9 23 iscygd 
 |-  ( T. -> ZZring e. CycGrp )
25 24 mptru 
 |-  ZZring e. CycGrp