Metamath Proof Explorer

Theorem iscygodd

Description: Show that a group with an element the same order as the group is cyclic. (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Hypotheses iscygodd.1 ⊢B=BaseG
iscygodd.o ⊢O=od⁡G
iscygodd.3 ⊢φ→G∈Grp
iscygodd.4 ⊢φ→X∈B
iscygodd.5 ⊢φ→O⁡X=B
Assertion iscygodd ⊢φ→G∈CycGrp

Proof

Step Hyp Ref Expression
1 iscygodd.1 ⊢B=BaseG
2 iscygodd.o ⊢O=od⁡G
3 iscygodd.3 ⊢φ→G∈Grp
4 iscygodd.4 ⊢φ→X∈B
5 iscygodd.5 ⊢φ→O⁡X=B
6 1 2 odcl ⊢X∈B→O⁡X∈ℕ0
7 4 6 syl ⊢φ→O⁡X∈ℕ0
8 5 7 eqeltrrd ⊢φ→B∈ℕ0
9 1 fvexi ⊢B∈V
10 hashclb ⊢B∈V→B∈Fin↔B∈ℕ0
11 9 10 ax-mp ⊢B∈Fin↔B∈ℕ0
12 8 11 sylibr ⊢φ→B∈Fin
13 eqid ⊢⋅G=⋅G
14 eqid ⊢x∈B|ran⁡n∈ℤ⟼n⋅Gx=B=x∈B|ran⁡n∈ℤ⟼n⋅Gx=B
15 1 13 14 2 cyggenod ⊢G∈Grp∧B∈Fin→X∈x∈B|ran⁡n∈ℤ⟼n⋅Gx=B↔X∈B∧O⁡X=B
16 3 12 15 syl2anc ⊢φ→X∈x∈B|ran⁡n∈ℤ⟼n⋅Gx=B↔X∈B∧O⁡X=B
17 4 5 16 mpbir2and ⊢φ→X∈x∈B|ran⁡n∈ℤ⟼n⋅Gx=B
18 17 ne0d ⊢φ→x∈B|ran⁡n∈ℤ⟼n⋅Gx=B≠∅
19 1 13 14 iscyg2 ⊢G∈CycGrp↔G∈Grp∧x∈B|ran⁡n∈ℤ⟼n⋅Gx=B≠∅
20 3 18 19 sylanbrc ⊢φ→G∈CycGrp