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 = Base G
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 = Base G
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 ⋅ G x = B = x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B
15 1 13 14 2 cyggenod ⊢ G ∈ Grp ∧ B ∈ Fin → X ∈ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B ↔ X ∈ B ∧ O ⁡ X = B
16 3 12 15 syl2anc ⊢ φ → X ∈ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B ↔ X ∈ B ∧ O ⁡ X = B
17 4 5 16 mpbir2and ⊢ φ → X ∈ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B
18 17 ne0d ⊢ φ → x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B ≠ ∅
19 1 13 14 iscyg2 ⊢ G ∈ CycGrp ↔ G ∈ Grp ∧ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B ≠ ∅
20 3 18 19 sylanbrc ⊢ φ → G ∈ CycGrp