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

Metamath Proof Explorer

Theorem cygzn

Description: A cyclic group with n elements is isomorphic to ZZ / n ZZ , and an infinite cyclic group is isomorphic to ZZ / 0 ZZ ~ZZ . (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses cygzn.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
cygzn.n ⊢ 𝑁 = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 )
cygzn.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
Assertion cygzn ( 𝐺 ∈ CycGrp → 𝐺 ≃𝑔 𝑌 )

Proof

Step Hyp Ref Expression
1 cygzn.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 cygzn.n ⊢ 𝑁 = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 )
3 cygzn.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
4 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
5 eqid ⊢ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } = { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 }
6 1 4 5 iscyg2 ⊢ ( 𝐺 ∈ CycGrp ↔ ( 𝐺 ∈ Grp ∧ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } ≠ ∅ ) )
7 6 simprbi ⊢ ( 𝐺 ∈ CycGrp → { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } ≠ ∅ )
8 n0 ⊢ ( { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } ≠ ∅ ↔ ∃ 𝑔 𝑔 ∈ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } )
9 7 8 sylib ⊢ ( 𝐺 ∈ CycGrp → ∃ 𝑔 𝑔 ∈ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } )
10 eqid ⊢ ( ℤRHom ‘ 𝑌 ) = ( ℤRHom ‘ 𝑌 )
11 simpl ⊢ ( ( 𝐺 ∈ CycGrp ∧ 𝑔 ∈ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } ) → 𝐺 ∈ CycGrp )
12 simpr ⊢ ( ( 𝐺 ∈ CycGrp ∧ 𝑔 ∈ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } ) → 𝑔 ∈ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } )
13 eqid ⊢ ran ( 𝑚 ∈ ℤ ↦ ⟨ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑚 ) , ( 𝑚 ( .g ‘ 𝐺 ) 𝑔 ) ⟩ ) = ran ( 𝑚 ∈ ℤ ↦ ⟨ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑚 ) , ( 𝑚 ( .g ‘ 𝐺 ) 𝑔 ) ⟩ )
14 1 2 3 4 10 5 11 12 13 cygznlem3 ⊢ ( ( 𝐺 ∈ CycGrp ∧ 𝑔 ∈ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } ) → 𝐺 ≃𝑔 𝑌 )
15 9 14 exlimddv ⊢ ( 𝐺 ∈ CycGrp → 𝐺 ≃𝑔 𝑌 )