This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC ALGEBRAIC STRUCTURES The complex numbers as an algebraic extensible structure Ring of integers 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 ‘ ℂfld ) ↾s ℤ ) = ( mulGrp ‘ ℤring )
Proof
Step
Hyp
Ref
Expression
1
cndrng ⊢ ℂfld ∈ DivRing
2
zex ⊢ ℤ ∈ V
3
df-zring ⊢ ℤring = ( ℂfld ↾s ℤ )
4
eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
5
3 4
mgpress ⊢ ( ( ℂfld ∈ DivRing ∧ ℤ ∈ V ) → ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) = ( mulGrp ‘ ℤring ) )
6
1 2 5
mp2an ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) = ( mulGrp ‘ ℤring )