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 → 𝐺 ≃𝑔 𝑌 )