Metamath Proof Explorer

Theorem cyggexb

Description: A finite abelian group is cyclic iff the exponent equals the order of the group. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses cygctb.1 ⊢ B = Base G
cyggex.o ⊢ E = gEx ⁡ G
Assertion cyggexb ⊢ G ∈ Abel ∧ B ∈ Fin → G ∈ CycGrp ↔ E = B

Proof

Step Hyp Ref Expression
1 cygctb.1 ⊢ B = Base G
2 cyggex.o ⊢ E = gEx ⁡ G
3 1 2 cyggex ⊢ G ∈ CycGrp ∧ B ∈ Fin → E = B
4 3 expcom ⊢ B ∈ Fin → G ∈ CycGrp → E = B
5 4 adantl ⊢ G ∈ Abel ∧ B ∈ Fin → G ∈ CycGrp → E = B
6 simpll ⊢ G ∈ Abel ∧ B ∈ Fin ∧ E = B → G ∈ Abel
7 ablgrp ⊢ G ∈ Abel → G ∈ Grp
8 7 ad2antrr ⊢ G ∈ Abel ∧ B ∈ Fin ∧ E = B → G ∈ Grp
9 simplr ⊢ G ∈ Abel ∧ B ∈ Fin ∧ E = B → B ∈ Fin
10 1 2 gexcl2 ⊢ G ∈ Grp ∧ B ∈ Fin → E ∈ ℕ
11 8 9 10 syl2anc ⊢ G ∈ Abel ∧ B ∈ Fin ∧ E = B → E ∈ ℕ
12 eqid ⊢ od ⁡ G = od ⁡ G
13 1 2 12 gexex ⊢ G ∈ Abel ∧ E ∈ ℕ → ∃ x ∈ B od ⁡ G ⁡ x = E
14 6 11 13 syl2anc ⊢ G ∈ Abel ∧ B ∈ Fin ∧ E = B → ∃ x ∈ B od ⁡ G ⁡ x = E
15 simplr ⊢ G ∈ Abel ∧ B ∈ Fin ∧ E = B ∧ x ∈ B → E = B
16 15 eqeq2d ⊢ G ∈ Abel ∧ B ∈ Fin ∧ E = B ∧ x ∈ B → od ⁡ G ⁡ x = E ↔ od ⁡ G ⁡ x = B
17 eqid ⊢ ⋅ G = ⋅ G
18 eqid ⊢ y ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G y = B = y ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G y = B
19 1 17 18 12 cyggenod ⊢ G ∈ Grp ∧ B ∈ Fin → x ∈ y ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G y = B ↔ x ∈ B ∧ od ⁡ G ⁡ x = B
20 8 9 19 syl2anc ⊢ G ∈ Abel ∧ B ∈ Fin ∧ E = B → x ∈ y ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G y = B ↔ x ∈ B ∧ od ⁡ G ⁡ x = B
21 ne0i ⊢ x ∈ y ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G y = B → y ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G y = B ≠ ∅
22 1 17 18 iscyg2 ⊢ G ∈ CycGrp ↔ G ∈ Grp ∧ y ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G y = B ≠ ∅
23 22 baib ⊢ G ∈ Grp → G ∈ CycGrp ↔ y ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G y = B ≠ ∅
24 8 23 syl ⊢ G ∈ Abel ∧ B ∈ Fin ∧ E = B → G ∈ CycGrp ↔ y ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G y = B ≠ ∅
25 21 24 syl5ibr ⊢ G ∈ Abel ∧ B ∈ Fin ∧ E = B → x ∈ y ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G y = B → G ∈ CycGrp
26 20 25 sylbird ⊢ G ∈ Abel ∧ B ∈ Fin ∧ E = B → x ∈ B ∧ od ⁡ G ⁡ x = B → G ∈ CycGrp
27 26 expdimp ⊢ G ∈ Abel ∧ B ∈ Fin ∧ E = B ∧ x ∈ B → od ⁡ G ⁡ x = B → G ∈ CycGrp
28 16 27 sylbid ⊢ G ∈ Abel ∧ B ∈ Fin ∧ E = B ∧ x ∈ B → od ⁡ G ⁡ x = E → G ∈ CycGrp
29 28 rexlimdva ⊢ G ∈ Abel ∧ B ∈ Fin ∧ E = B → ∃ x ∈ B od ⁡ G ⁡ x = E → G ∈ CycGrp
30 14 29 mpd ⊢ G ∈ Abel ∧ B ∈ Fin ∧ E = B → G ∈ CycGrp
31 30 ex ⊢ G ∈ Abel ∧ B ∈ Fin → E = B → G ∈ CycGrp
32 5 31 impbid ⊢ G ∈ Abel ∧ B ∈ Fin → G ∈ CycGrp ↔ E = B