Theorem cyggenod

Description: An element is the generator of a finite group iff the order of the generator equals the order of the group. (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	iscyg.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
	iscyg.2	⊢ · = ( .g ‘ 𝐺 )
	iscyg3.e	⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 }
	cyggenod.o	⊢ 𝑂 = ( od ‘ 𝐺 )
Assertion	cyggenod	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) → ( 𝑋 ∈ 𝐸 ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑋 ) = ( ♯ ‘ 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscyg.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		iscyg.2	⊢ · = ( .g ‘ 𝐺 )
3		iscyg3.e	⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 }
4		cyggenod.o	⊢ 𝑂 = ( od ‘ 𝐺 )
5	1 2 3	iscyggen	⊢ ( 𝑋 ∈ 𝐸 ↔ ( 𝑋 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = 𝐵 ) )
6		simplr	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) ∧ 𝑋 ∈ 𝐵 ) → 𝐵 ∈ Fin )
7		simplll	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℤ ) → 𝐺 ∈ Grp )
8		simpr	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℤ )
9		simplr	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℤ ) → 𝑋 ∈ 𝐵 )
10	1 2	mulgcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑛 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑛 · 𝑋 ) ∈ 𝐵 )
11	7 8 9 10	syl3anc	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℤ ) → ( 𝑛 · 𝑋 ) ∈ 𝐵 )
12	11	fmpttd	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) : ℤ ⟶ 𝐵 )
13	12	frnd	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) ∧ 𝑋 ∈ 𝐵 ) → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ⊆ 𝐵 )
14	6 13	ssfid	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) ∧ 𝑋 ∈ 𝐵 ) → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ∈ Fin )
15		hashen	⊢ ( ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ) = ( ♯ ‘ 𝐵 ) ↔ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ≈ 𝐵 ) )
16	14 6 15	syl2anc	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) ∧ 𝑋 ∈ 𝐵 ) → ( ( ♯ ‘ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ) = ( ♯ ‘ 𝐵 ) ↔ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ≈ 𝐵 ) )
17		eqid	⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) )
18	1 4 2 17	dfod2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑂 ‘ 𝑋 ) = if ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ∈ Fin , ( ♯ ‘ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ) , 0 ) )
19	18	adantlr	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝑂 ‘ 𝑋 ) = if ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ∈ Fin , ( ♯ ‘ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ) , 0 ) )
20	14	iftrued	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) ∧ 𝑋 ∈ 𝐵 ) → if ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ∈ Fin , ( ♯ ‘ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ) , 0 ) = ( ♯ ‘ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ) )
21	19 20	eqtr2d	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) ∧ 𝑋 ∈ 𝐵 ) → ( ♯ ‘ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ) = ( 𝑂 ‘ 𝑋 ) )
22	21	eqeq1d	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) ∧ 𝑋 ∈ 𝐵 ) → ( ( ♯ ‘ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ) = ( ♯ ‘ 𝐵 ) ↔ ( 𝑂 ‘ 𝑋 ) = ( ♯ ‘ 𝐵 ) ) )
23		fisseneq	⊢ ( ( 𝐵 ∈ Fin ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ⊆ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ≈ 𝐵 ) → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = 𝐵 )
24	23	3expia	⊢ ( ( 𝐵 ∈ Fin ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ⊆ 𝐵 ) → ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ≈ 𝐵 → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = 𝐵 ) )
25		enrefg	⊢ ( 𝐵 ∈ Fin → 𝐵 ≈ 𝐵 )
26	25	adantr	⊢ ( ( 𝐵 ∈ Fin ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ⊆ 𝐵 ) → 𝐵 ≈ 𝐵 )
27		breq1	⊢ ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = 𝐵 → ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ≈ 𝐵 ↔ 𝐵 ≈ 𝐵 ) )
28	26 27	syl5ibrcom	⊢ ( ( 𝐵 ∈ Fin ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ⊆ 𝐵 ) → ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = 𝐵 → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ≈ 𝐵 ) )
29	24 28	impbid	⊢ ( ( 𝐵 ∈ Fin ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ⊆ 𝐵 ) → ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ≈ 𝐵 ↔ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = 𝐵 ) )
30	6 13 29	syl2anc	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) ∧ 𝑋 ∈ 𝐵 ) → ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ≈ 𝐵 ↔ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = 𝐵 ) )
31	16 22 30	3bitr3rd	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) ∧ 𝑋 ∈ 𝐵 ) → ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = 𝐵 ↔ ( 𝑂 ‘ 𝑋 ) = ( ♯ ‘ 𝐵 ) ) )
32	31	pm5.32da	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) → ( ( 𝑋 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = 𝐵 ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑋 ) = ( ♯ ‘ 𝐵 ) ) ) )
33	5 32	bitrid	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) → ( 𝑋 ∈ 𝐸 ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑋 ) = ( ♯ ‘ 𝐵 ) ) ) )