Metamath Proof Explorer

Theorem cyggic

Description: Cyclic groups are isomorphic precisely when they have the same order. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses cygctb.b ⊢B=BaseG
cygctb.c ⊢C=BaseH
Assertion cyggic ⊢G∈CycGrp∧H∈CycGrp→G≃𝑔H↔B≈C

Proof

Step Hyp Ref Expression
1 cygctb.b ⊢B=BaseG
2 cygctb.c ⊢C=BaseH
3 1 2 gicen ⊢G≃𝑔H→B≈C
4 eqid ⊢ifB∈FinB0=ifB∈FinB0
5 eqid ⊢ℤ/ifB∈FinB0ℤ=ℤ/ifB∈FinB0ℤ
6 1 4 5 cygzn ⊢G∈CycGrp→G≃𝑔ℤ/ifB∈FinB0ℤ
7 6 ad2antrr ⊢G∈CycGrp∧H∈CycGrp∧B≈C→G≃𝑔ℤ/ifB∈FinB0ℤ
8 enfi ⊢B≈C→B∈Fin↔C∈Fin
9 8 adantl ⊢G∈CycGrp∧H∈CycGrp∧B≈C→B∈Fin↔C∈Fin
10 hasheni ⊢B≈C→B=C
11 10 adantl ⊢G∈CycGrp∧H∈CycGrp∧B≈C→B=C
12 9 11 ifbieq1d ⊢G∈CycGrp∧H∈CycGrp∧B≈C→ifB∈FinB0=ifC∈FinC0
13 12 fveq2d ⊢G∈CycGrp∧H∈CycGrp∧B≈C→ℤ/ifB∈FinB0ℤ=ℤ/ifC∈FinC0ℤ
14 eqid ⊢ifC∈FinC0=ifC∈FinC0
15 eqid ⊢ℤ/ifC∈FinC0ℤ=ℤ/ifC∈FinC0ℤ
16 2 14 15 cygzn ⊢H∈CycGrp→H≃𝑔ℤ/ifC∈FinC0ℤ
17 16 ad2antlr ⊢G∈CycGrp∧H∈CycGrp∧B≈C→H≃𝑔ℤ/ifC∈FinC0ℤ
18 gicsym ⊢H≃𝑔ℤ/ifC∈FinC0ℤ→ℤ/ifC∈FinC0ℤ≃𝑔H
19 17 18 syl ⊢G∈CycGrp∧H∈CycGrp∧B≈C→ℤ/ifC∈FinC0ℤ≃𝑔H
20 13 19 eqbrtrd ⊢G∈CycGrp∧H∈CycGrp∧B≈C→ℤ/ifB∈FinB0ℤ≃𝑔H
21 gictr ⊢G≃𝑔ℤ/ifB∈FinB0ℤ∧ℤ/ifB∈FinB0ℤ≃𝑔H→G≃𝑔H
22 7 20 21 syl2anc ⊢G∈CycGrp∧H∈CycGrp∧B≈C→G≃𝑔H
23 22 ex ⊢G∈CycGrp∧H∈CycGrp→B≈C→G≃𝑔H
24 3 23 impbid2 ⊢G∈CycGrp∧H∈CycGrp→G≃𝑔H↔B≈C