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 = Base G
cygctb.c ⊢ C = Base H
Assertion cyggic ⊢ G ∈ CycGrp ∧ H ∈ CycGrp → G ≃ 𝑔 H ↔ B ≈ C

Proof

Step Hyp Ref Expression
1 cygctb.b ⊢ B = Base G
2 cygctb.c ⊢ C = Base H
3 1 2 gicen ⊢ G ≃ 𝑔 H → B ≈ C
4 eqid ⊢ if B ∈ Fin B 0 = if B ∈ Fin B 0
5 eqid ⊢ ℤ/ if B ∈ Fin B 0 ℤ = ℤ/ if B ∈ Fin B 0 ℤ
6 1 4 5 cygzn ⊢ G ∈ CycGrp → G ≃ 𝑔 ℤ/ if B ∈ Fin B 0 ℤ
7 6 ad2antrr ⊢ G ∈ CycGrp ∧ H ∈ CycGrp ∧ B ≈ C → G ≃ 𝑔 ℤ/ if B ∈ Fin B 0 ℤ
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 → if B ∈ Fin B 0 = if C ∈ Fin C 0
13 12 fveq2d ⊢ G ∈ CycGrp ∧ H ∈ CycGrp ∧ B ≈ C → ℤ/ if B ∈ Fin B 0 ℤ = ℤ/ if C ∈ Fin C 0 ℤ
14 eqid ⊢ if C ∈ Fin C 0 = if C ∈ Fin C 0
15 eqid ⊢ ℤ/ if C ∈ Fin C 0 ℤ = ℤ/ if C ∈ Fin C 0 ℤ
16 2 14 15 cygzn ⊢ H ∈ CycGrp → H ≃ 𝑔 ℤ/ if C ∈ Fin C 0 ℤ
17 16 ad2antlr ⊢ G ∈ CycGrp ∧ H ∈ CycGrp ∧ B ≈ C → H ≃ 𝑔 ℤ/ if C ∈ Fin C 0 ℤ
18 gicsym ⊢ H ≃ 𝑔 ℤ/ if C ∈ Fin C 0 ℤ → ℤ/ if C ∈ Fin C 0 ℤ ≃ 𝑔 H
19 17 18 syl ⊢ G ∈ CycGrp ∧ H ∈ CycGrp ∧ B ≈ C → ℤ/ if C ∈ Fin C 0 ℤ ≃ 𝑔 H
20 13 19 eqbrtrd ⊢ G ∈ CycGrp ∧ H ∈ CycGrp ∧ B ≈ C → ℤ/ if B ∈ Fin B 0 ℤ ≃ 𝑔 H
21 gictr ⊢ G ≃ 𝑔 ℤ/ if B ∈ Fin B 0 ℤ ∧ ℤ/ if B ∈ Fin B 0 ℤ ≃ 𝑔 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