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 imbitrrid ⊢ ( ( ( 𝐺 ∈ 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 ↔ 𝐸 = ( ♯ ‘ 𝐵 ) ) )