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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	iscygodd.o	⊢ 𝑂 = ( od ‘ 𝐺 )
	iscygodd.3	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	iscygodd.4	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	iscygodd.5	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) = ( ♯ ‘ 𝐵 ) )
Assertion	iscygodd	⊢ ( 𝜑 → 𝐺 ∈ CycGrp )

Proof

Step	Hyp	Ref	Expression
1		iscygodd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		iscygodd.o	⊢ 𝑂 = ( od ‘ 𝐺 )
3		iscygodd.3	⊢ ( 𝜑 → 𝐺 ∈ Grp )
4		iscygodd.4	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		iscygodd.5	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) = ( ♯ ‘ 𝐵 ) )
6	1 2	odcl	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑂 ‘ 𝑋 ) ∈ ℕ0 )
7	4 6	syl	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) ∈ ℕ0 )
8	5 7	eqeltrrd	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
9	1	fvexi	⊢ 𝐵 ∈ V
10		hashclb	⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ Fin ↔ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) )
11	9 10	ax-mp	⊢ ( 𝐵 ∈ Fin ↔ ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
12	8 11	sylibr	⊢ ( 𝜑 → 𝐵 ∈ Fin )
13		eqid	⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
14		eqid	⊢ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } = { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 }
15	1 13 14 2	cyggenod	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) → ( 𝑋 ∈ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑋 ) = ( ♯ ‘ 𝐵 ) ) ) )
16	3 12 15	syl2anc	⊢ ( 𝜑 → ( 𝑋 ∈ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑋 ) = ( ♯ ‘ 𝐵 ) ) ) )
17	4 5 16	mpbir2and	⊢ ( 𝜑 → 𝑋 ∈ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } )
18	17	ne0d	⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } ≠ ∅ )
19	1 13 14	iscyg2	⊢ ( 𝐺 ∈ CycGrp ↔ ( 𝐺 ∈ Grp ∧ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } ≠ ∅ ) )
20	3 18 19	sylanbrc	⊢ ( 𝜑 → 𝐺 ∈ CycGrp )