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 𝐵 = ( Base ‘ 𝐺 )
cyggex.o 𝐸 = ( gEx ‘ 𝐺 )
Assertion cyggexb ( ( 𝐺 ∈ Abel ∧ 𝐵 ∈ Fin ) → ( 𝐺 ∈ CycGrp ↔ 𝐸 = ( ♯ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 cygctb.1 𝐵 = ( Base ‘ 𝐺 )
2 cyggex.o 𝐸 = ( gEx ‘ 𝐺 )
3 1 2 cyggex ( ( 𝐺 ∈ CycGrp ∧ 𝐵 ∈ Fin ) → 𝐸 = ( ♯ ‘ 𝐵 ) )
4 3 expcom ( 𝐵 ∈ Fin → ( 𝐺 ∈ CycGrp → 𝐸 = ( ♯ ‘ 𝐵 ) ) )
5 4 adantl ( ( 𝐺 ∈ Abel ∧ 𝐵 ∈ Fin ) → ( 𝐺 ∈ CycGrp → 𝐸 = ( ♯ ‘ 𝐵 ) ) )
6 simpll ( ( ( 𝐺 ∈ Abel ∧ 𝐵 ∈ Fin ) ∧ 𝐸 = ( ♯ ‘ 𝐵 ) ) → 𝐺 ∈ Abel )
7 ablgrp ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
8 7 ad2antrr ( ( ( 𝐺 ∈ Abel ∧ 𝐵 ∈ Fin ) ∧ 𝐸 = ( ♯ ‘ 𝐵 ) ) → 𝐺 ∈ Grp )
9 simplr ( ( ( 𝐺 ∈ Abel ∧ 𝐵 ∈ Fin ) ∧ 𝐸 = ( ♯ ‘ 𝐵 ) ) → 𝐵 ∈ Fin )
10 1 2 gexcl2 ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) → 𝐸 ∈ ℕ )
11 8 9 10 syl2anc ( ( ( 𝐺 ∈ Abel ∧ 𝐵 ∈ Fin ) ∧ 𝐸 = ( ♯ ‘ 𝐵 ) ) → 𝐸 ∈ ℕ )
12 eqid ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
13 1 2 12 gexex ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → ∃ 𝑥𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐸 )
14 6 11 13 syl2anc ( ( ( 𝐺 ∈ Abel ∧ 𝐵 ∈ Fin ) ∧ 𝐸 = ( ♯ ‘ 𝐵 ) ) → ∃ 𝑥𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐸 )
15 simplr ( ( ( ( 𝐺 ∈ Abel ∧ 𝐵 ∈ Fin ) ∧ 𝐸 = ( ♯ ‘ 𝐵 ) ) ∧ 𝑥𝐵 ) → 𝐸 = ( ♯ ‘ 𝐵 ) )
16 15 eqeq2d ( ( ( ( 𝐺 ∈ Abel ∧ 𝐵 ∈ Fin ) ∧ 𝐸 = ( ♯ ‘ 𝐵 ) ) ∧ 𝑥𝐵 ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐸 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ) )
17 eqid ( .g𝐺 ) = ( .g𝐺 )
18 eqid { 𝑦𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g𝐺 ) 𝑦 ) ) = 𝐵 } = { 𝑦𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g𝐺 ) 𝑦 ) ) = 𝐵 }
19 1 17 18 12 cyggenod ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) → ( 𝑥 ∈ { 𝑦𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g𝐺 ) 𝑦 ) ) = 𝐵 } ↔ ( 𝑥𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ) ) )
20 8 9 19 syl2anc ( ( ( 𝐺 ∈ Abel ∧ 𝐵 ∈ Fin ) ∧ 𝐸 = ( ♯ ‘ 𝐵 ) ) → ( 𝑥 ∈ { 𝑦𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g𝐺 ) 𝑦 ) ) = 𝐵 } ↔ ( 𝑥𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ) ) )
21 ne0i ( 𝑥 ∈ { 𝑦𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g𝐺 ) 𝑦 ) ) = 𝐵 } → { 𝑦𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g𝐺 ) 𝑦 ) ) = 𝐵 } ≠ ∅ )
22 1 17 18 iscyg2 ( 𝐺 ∈ CycGrp ↔ ( 𝐺 ∈ Grp ∧ { 𝑦𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g𝐺 ) 𝑦 ) ) = 𝐵 } ≠ ∅ ) )
23 22 baib ( 𝐺 ∈ Grp → ( 𝐺 ∈ CycGrp ↔ { 𝑦𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g𝐺 ) 𝑦 ) ) = 𝐵 } ≠ ∅ ) )
24 8 23 syl ( ( ( 𝐺 ∈ Abel ∧ 𝐵 ∈ Fin ) ∧ 𝐸 = ( ♯ ‘ 𝐵 ) ) → ( 𝐺 ∈ CycGrp ↔ { 𝑦𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g𝐺 ) 𝑦 ) ) = 𝐵 } ≠ ∅ ) )
25 21 24 syl5ibr ( ( ( 𝐺 ∈ Abel ∧ 𝐵 ∈ Fin ) ∧ 𝐸 = ( ♯ ‘ 𝐵 ) ) → ( 𝑥 ∈ { 𝑦𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g𝐺 ) 𝑦 ) ) = 𝐵 } → 𝐺 ∈ CycGrp ) )
26 20 25 sylbird ( ( ( 𝐺 ∈ Abel ∧ 𝐵 ∈ Fin ) ∧ 𝐸 = ( ♯ ‘ 𝐵 ) ) → ( ( 𝑥𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ) → 𝐺 ∈ CycGrp ) )
27 26 expdimp ( ( ( ( 𝐺 ∈ Abel ∧ 𝐵 ∈ Fin ) ∧ 𝐸 = ( ♯ ‘ 𝐵 ) ) ∧ 𝑥𝐵 ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) → 𝐺 ∈ CycGrp ) )
28 16 27 sylbid ( ( ( ( 𝐺 ∈ Abel ∧ 𝐵 ∈ Fin ) ∧ 𝐸 = ( ♯ ‘ 𝐵 ) ) ∧ 𝑥𝐵 ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐸𝐺 ∈ CycGrp ) )
29 28 rexlimdva ( ( ( 𝐺 ∈ Abel ∧ 𝐵 ∈ Fin ) ∧ 𝐸 = ( ♯ ‘ 𝐵 ) ) → ( ∃ 𝑥𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐸𝐺 ∈ CycGrp ) )
30 14 29 mpd ( ( ( 𝐺 ∈ Abel ∧ 𝐵 ∈ Fin ) ∧ 𝐸 = ( ♯ ‘ 𝐵 ) ) → 𝐺 ∈ CycGrp )
31 30 ex ( ( 𝐺 ∈ Abel ∧ 𝐵 ∈ Fin ) → ( 𝐸 = ( ♯ ‘ 𝐵 ) → 𝐺 ∈ CycGrp ) )
32 5 31 impbid ( ( 𝐺 ∈ Abel ∧ 𝐵 ∈ Fin ) → ( 𝐺 ∈ CycGrp ↔ 𝐸 = ( ♯ ‘ 𝐵 ) ) )