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 ) ) )
5 4 adantl 
 |-  ( ( 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 )
8 7 ad2antrr 
 |-  ( ( ( 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 imbitrrid 
 |-  ( ( ( 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 ) ) )