Metamath Proof Explorer

Theorem cygth

Description: The "fundamental theorem of cyclic groups". Cyclic groups are exactly the additive groups ZZ / n ZZ , for 0 <_ n (where n = 0 is the infinite cyclic group ZZ ), up to isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Assertion cygth ⊢ G ∈ CycGrp ↔ ∃ n ∈ ℕ 0 G ≃ 𝑔 ℤ/nℤ

Proof

Step Hyp Ref Expression
1 hashcl ⊢ Base G ∈ Fin → Base G ∈ ℕ 0
2 1 adantl ⊢ G ∈ CycGrp ∧ Base G ∈ Fin → Base G ∈ ℕ 0
3 0nn0 ⊢ 0 ∈ ℕ 0
4 3 a1i ⊢ G ∈ CycGrp ∧ ¬ Base G ∈ Fin → 0 ∈ ℕ 0
5 2 4 ifclda ⊢ G ∈ CycGrp → if Base G ∈ Fin Base G 0 ∈ ℕ 0
6 eqid ⊢ Base G = Base G
7 eqid ⊢ if Base G ∈ Fin Base G 0 = if Base G ∈ Fin Base G 0
8 eqid ⊢ ℤ/ if Base G ∈ Fin Base G 0 ℤ = ℤ/ if Base G ∈ Fin Base G 0 ℤ
9 6 7 8 cygzn ⊢ G ∈ CycGrp → G ≃ 𝑔 ℤ/ if Base G ∈ Fin Base G 0 ℤ
10 fveq2 ⊢ n = if Base G ∈ Fin Base G 0 → ℤ/nℤ = ℤ/ if Base G ∈ Fin Base G 0 ℤ
11 10 breq2d ⊢ n = if Base G ∈ Fin Base G 0 → G ≃ 𝑔 ℤ/nℤ ↔ G ≃ 𝑔 ℤ/ if Base G ∈ Fin Base G 0 ℤ
12 11 rspcev ⊢ if Base G ∈ Fin Base G 0 ∈ ℕ 0 ∧ G ≃ 𝑔 ℤ/ if Base G ∈ Fin Base G 0 ℤ → ∃ n ∈ ℕ 0 G ≃ 𝑔 ℤ/nℤ
13 5 9 12 syl2anc ⊢ G ∈ CycGrp → ∃ n ∈ ℕ 0 G ≃ 𝑔 ℤ/nℤ
14 gicsym ⊢ G ≃ 𝑔 ℤ/nℤ → ℤ/nℤ ≃ 𝑔 G
15 eqid ⊢ ℤ/nℤ = ℤ/nℤ
16 15 zncyg ⊢ n ∈ ℕ 0 → ℤ/nℤ ∈ CycGrp
17 giccyg ⊢ ℤ/nℤ ≃ 𝑔 G → ℤ/nℤ ∈ CycGrp → G ∈ CycGrp
18 14 16 17 syl2imc ⊢ n ∈ ℕ 0 → G ≃ 𝑔 ℤ/nℤ → G ∈ CycGrp
19 18 rexlimiv ⊢ ∃ n ∈ ℕ 0 G ≃ 𝑔 ℤ/nℤ → G ∈ CycGrp
20 13 19 impbii ⊢ G ∈ CycGrp ↔ ∃ n ∈ ℕ 0 G ≃ 𝑔 ℤ/nℤ