Theorem zringmpg

Description: The multiplicative group of the ring of integers is the restriction of the multiplicative group of the complex numbers to the integers. (Contributed by AV, 15-Jun-2019)

	Ref	Expression
Assertion	zringmpg	|- ( ( mulGrp ` CCfld ) |`s ZZ ) = ( mulGrp ` ZZring )

Proof

Step	Hyp	Ref	Expression
1		cndrng	|- CCfld e. DivRing
2		zex	|- ZZ e. _V
3		df-zring	|- ZZring = ( CCfld |`s ZZ )
4		eqid	|- ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
5	3 4	mgpress	|- ( ( CCfld e. DivRing /\ ZZ e. _V ) -> ( ( mulGrp ` CCfld ) |`s ZZ ) = ( mulGrp ` ZZring ) )
6	1 2 5	mp2an	|- ( ( mulGrp ` CCfld ) |`s ZZ ) = ( mulGrp ` ZZring )