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=BaseG
cyggex.o ⊢E=gEx⁡G
Assertion cyggexb ⊢G∈Abel∧B∈Fin→G∈CycGrp↔E=B

Proof

Step Hyp Ref Expression
1 cygctb.1 ⊢B=BaseG
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∈Bod⁡G⁡x=E
14 6 11 13 syl2anc ⊢G∈Abel∧B∈Fin∧E=B→∃x∈Bod⁡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⋅Gy=B=y∈B|ran⁡n∈ℤ⟼n⋅Gy=B
19 1 17 18 12 cyggenod ⊢G∈Grp∧B∈Fin→x∈y∈B|ran⁡n∈ℤ⟼n⋅Gy=B↔x∈B∧od⁡G⁡x=B
20 8 9 19 syl2anc ⊢G∈Abel∧B∈Fin∧E=B→x∈y∈B|ran⁡n∈ℤ⟼n⋅Gy=B↔x∈B∧od⁡G⁡x=B
21 ne0i ⊢x∈y∈B|ran⁡n∈ℤ⟼n⋅Gy=B→y∈B|ran⁡n∈ℤ⟼n⋅Gy=B≠∅
22 1 17 18 iscyg2 ⊢G∈CycGrp↔G∈Grp∧y∈B|ran⁡n∈ℤ⟼n⋅Gy=B≠∅
23 22 baib ⊢G∈Grp→G∈CycGrp↔y∈B|ran⁡n∈ℤ⟼n⋅Gy=B≠∅
24 8 23 syl ⊢G∈Abel∧B∈Fin∧E=B→G∈CycGrp↔y∈B|ran⁡n∈ℤ⟼n⋅Gy=B≠∅
25 21 24 imbitrrid ⊢G∈Abel∧B∈Fin∧E=B→x∈y∈B|ran⁡n∈ℤ⟼n⋅Gy=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∈Bod⁡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