| 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
|
mulridd |
|- ( 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 |