This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ℤring ∈ CycGrp

Proof

Step Hyp Ref Expression
1 zringbas ⊢ ℤ = ( Base ‘ ℤring )
2 eqid ⊢ ( .g ‘ ℤring ) = ( .g ‘ ℤring )
3 zsubrg ⊢ ℤ ∈ ( SubRing ‘ ℂfld )
4 subrgsubg ⊢ ( ℤ ∈ ( SubRing ‘ ℂfld ) → ℤ ∈ ( SubGrp ‘ ℂfld ) )
5 3 4 ax-mp ⊢ ℤ ∈ ( SubGrp ‘ ℂfld )
6 df-zring ⊢ ℤring = ( ℂfld ↾s ℤ )
7 6 subggrp ⊢ ( ℤ ∈ ( SubGrp ‘ ℂfld ) → ℤring ∈ Grp )
8 5 7 mp1i ⊢ ( ⊤ → ℤring ∈ Grp )
9 1zzd ⊢ ( ⊤ → 1 ∈ ℤ )
10 ax-1cn ⊢ 1 ∈ ℂ
11 cnfldmulg ⊢ ( ( 𝑥 ∈ ℤ ∧ 1 ∈ ℂ ) → ( 𝑥 ( .g ‘ ℂfld ) 1 ) = ( 𝑥 · 1 ) )
12 10 11 mpan2 ⊢ ( 𝑥 ∈ ℤ → ( 𝑥 ( .g ‘ ℂfld ) 1 ) = ( 𝑥 · 1 ) )
13 1z ⊢ 1 ∈ ℤ
14 eqid ⊢ ( .g ‘ ℂfld ) = ( .g ‘ ℂfld )
15 14 6 2 subgmulg ⊢ ( ( ℤ ∈ ( SubGrp ‘ ℂfld ) ∧ 𝑥 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝑥 ( .g ‘ ℂfld ) 1 ) = ( 𝑥 ( .g ‘ ℤring ) 1 ) )
16 5 13 15 mp3an13 ⊢ ( 𝑥 ∈ ℤ → ( 𝑥 ( .g ‘ ℂfld ) 1 ) = ( 𝑥 ( .g ‘ ℤring ) 1 ) )
17 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
18 17 mulridd ⊢ ( 𝑥 ∈ ℤ → ( 𝑥 · 1 ) = 𝑥 )
19 12 16 18 3eqtr3rd ⊢ ( 𝑥 ∈ ℤ → 𝑥 = ( 𝑥 ( .g ‘ ℤring ) 1 ) )
20 oveq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ( .g ‘ ℤring ) 1 ) = ( 𝑥 ( .g ‘ ℤring ) 1 ) )
21 20 rspceeqv ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑥 = ( 𝑥 ( .g ‘ ℤring ) 1 ) ) → ∃ 𝑧 ∈ ℤ 𝑥 = ( 𝑧 ( .g ‘ ℤring ) 1 ) )
22 19 21 mpdan ⊢ ( 𝑥 ∈ ℤ → ∃ 𝑧 ∈ ℤ 𝑥 = ( 𝑧 ( .g ‘ ℤring ) 1 ) )
23 22 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℤ ) → ∃ 𝑧 ∈ ℤ 𝑥 = ( 𝑧 ( .g ‘ ℤring ) 1 ) )
24 1 2 8 9 23 iscygd ⊢ ( ⊤ → ℤring ∈ CycGrp )
25 24 mptru ⊢ ℤring ∈ CycGrp