# 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
`|- B = ( Base ` G )`
cyggex.o
`|- E = ( gEx ` G )`
Assertion cyggexb
`|- ( ( G e. Abel /\ B e. Fin ) -> ( G e. CycGrp <-> E = ( # ` B ) ) )`

### Proof

Step Hyp Ref Expression
1 cygctb.1
` |-  B = ( Base ` G )`
2 cyggex.o
` |-  E = ( gEx ` G )`
3 1 2 cyggex
` |-  ( ( G e. CycGrp /\ B e. Fin ) -> E = ( # ` B ) )`
4 3 expcom
` |-  ( B e. Fin -> ( G e. CycGrp -> E = ( # ` B ) ) )`
` |-  ( ( G e. Abel /\ B e. Fin ) -> ( G e. CycGrp -> E = ( # ` B ) ) )`
6 simpll
` |-  ( ( ( G e. Abel /\ B e. Fin ) /\ E = ( # ` B ) ) -> G e. Abel )`
7 ablgrp
` |-  ( G e. Abel -> G e. Grp )`
` |-  ( ( ( G e. Abel /\ B e. Fin ) /\ E = ( # ` B ) ) -> G e. Grp )`
9 simplr
` |-  ( ( ( G e. Abel /\ B e. Fin ) /\ E = ( # ` B ) ) -> B e. Fin )`
10 1 2 gexcl2
` |-  ( ( G e. Grp /\ B e. Fin ) -> E e. NN )`
11 8 9 10 syl2anc
` |-  ( ( ( G e. Abel /\ B e. Fin ) /\ E = ( # ` B ) ) -> E e. NN )`
12 eqid
` |-  ( od ` G ) = ( od ` G )`
13 1 2 12 gexex
` |-  ( ( G e. Abel /\ E e. NN ) -> E. x e. B ( ( od ` G ) ` x ) = E )`
14 6 11 13 syl2anc
` |-  ( ( ( G e. Abel /\ B e. Fin ) /\ E = ( # ` B ) ) -> E. x e. B ( ( od ` G ) ` x ) = E )`
15 simplr
` |-  ( ( ( ( G e. Abel /\ B e. Fin ) /\ E = ( # ` B ) ) /\ x e. B ) -> E = ( # ` B ) )`
16 15 eqeq2d
` |-  ( ( ( ( G e. Abel /\ B e. Fin ) /\ E = ( # ` B ) ) /\ x e. B ) -> ( ( ( od ` G ) ` x ) = E <-> ( ( od ` G ) ` x ) = ( # ` B ) ) )`
17 eqid
` |-  ( .g ` G ) = ( .g ` G )`
18 eqid
` |-  { y e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B } = { y e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B }`
19 1 17 18 12 cyggenod
` |-  ( ( G e. Grp /\ B e. Fin ) -> ( x e. { y e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B } <-> ( x e. B /\ ( ( od ` G ) ` x ) = ( # ` B ) ) ) )`
20 8 9 19 syl2anc
` |-  ( ( ( G e. Abel /\ B e. Fin ) /\ E = ( # ` B ) ) -> ( x e. { y e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B } <-> ( x e. B /\ ( ( od ` G ) ` x ) = ( # ` B ) ) ) )`
21 ne0i
` |-  ( x e. { y e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B } -> { y e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B } =/= (/) )`
22 1 17 18 iscyg2
` |-  ( G e. CycGrp <-> ( G e. Grp /\ { y e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B } =/= (/) ) )`
23 22 baib
` |-  ( G e. Grp -> ( G e. CycGrp <-> { y e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B } =/= (/) ) )`
24 8 23 syl
` |-  ( ( ( G e. Abel /\ B e. Fin ) /\ E = ( # ` B ) ) -> ( G e. CycGrp <-> { y e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B } =/= (/) ) )`
25 21 24 syl5ibr
` |-  ( ( ( G e. Abel /\ B e. Fin ) /\ E = ( # ` B ) ) -> ( x e. { y e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B } -> G e. CycGrp ) )`
26 20 25 sylbird
` |-  ( ( ( G e. Abel /\ B e. Fin ) /\ E = ( # ` B ) ) -> ( ( x e. B /\ ( ( od ` G ) ` x ) = ( # ` B ) ) -> G e. CycGrp ) )`
27 26 expdimp
` |-  ( ( ( ( G e. Abel /\ B e. Fin ) /\ E = ( # ` B ) ) /\ x e. B ) -> ( ( ( od ` G ) ` x ) = ( # ` B ) -> G e. CycGrp ) )`
28 16 27 sylbid
` |-  ( ( ( ( G e. Abel /\ B e. Fin ) /\ E = ( # ` B ) ) /\ x e. B ) -> ( ( ( od ` G ) ` x ) = E -> G e. CycGrp ) )`
29 28 rexlimdva
` |-  ( ( ( G e. Abel /\ B e. Fin ) /\ E = ( # ` B ) ) -> ( E. x e. B ( ( od ` G ) ` x ) = E -> G e. CycGrp ) )`
30 14 29 mpd
` |-  ( ( ( G e. Abel /\ B e. Fin ) /\ E = ( # ` B ) ) -> G e. CycGrp )`
31 30 ex
` |-  ( ( G e. Abel /\ B e. Fin ) -> ( E = ( # ` B ) -> G e. CycGrp ) )`
32 5 31 impbid
` |-  ( ( G e. Abel /\ B e. Fin ) -> ( G e. CycGrp <-> E = ( # ` B ) ) )`