This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iscygodd

Description: Show that a group with an element the same order as the group is cyclic. (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Hypotheses iscygodd.1 
|- B = ( Base ` G )
iscygodd.o 
|- O = ( od ` G )
iscygodd.3 
|- ( ph -> G e. Grp )
iscygodd.4 
|- ( ph -> X e. B )
iscygodd.5 
|- ( ph -> ( O ` X ) = ( # ` B ) )
Assertion iscygodd 
|- ( ph -> G e. CycGrp )

Proof

Step Hyp Ref Expression
1 iscygodd.1 
 |-  B = ( Base ` G )
2 iscygodd.o 
 |-  O = ( od ` G )
3 iscygodd.3 
 |-  ( ph -> G e. Grp )
4 iscygodd.4 
 |-  ( ph -> X e. B )
5 iscygodd.5 
 |-  ( ph -> ( O ` X ) = ( # ` B ) )
6 1 2 odcl 
 |-  ( X e. B -> ( O ` X ) e. NN0 )
7 4 6 syl 
 |-  ( ph -> ( O ` X ) e. NN0 )
8 5 7 eqeltrrd 
 |-  ( ph -> ( # ` B ) e. NN0 )
9 1 fvexi 
 |-  B e. _V
10 hashclb 
 |-  ( B e. _V -> ( B e. Fin <-> ( # ` B ) e. NN0 ) )
11 9 10 ax-mp 
 |-  ( B e. Fin <-> ( # ` B ) e. NN0 )
12 8 11 sylibr 
 |-  ( ph -> B e. Fin )
13 eqid 
 |-  ( .g ` G ) = ( .g ` G )
14 eqid 
 |-  { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } = { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B }
15 1 13 14 2 cyggenod 
 |-  ( ( G e. Grp /\ B e. Fin ) -> ( X e. { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } <-> ( X e. B /\ ( O ` X ) = ( # ` B ) ) ) )
16 3 12 15 syl2anc 
 |-  ( ph -> ( X e. { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } <-> ( X e. B /\ ( O ` X ) = ( # ` B ) ) ) )
17 4 5 16 mpbir2and 
 |-  ( ph -> X e. { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } )
18 17 ne0d 
 |-  ( ph -> { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } =/= (/) )
19 1 13 14 iscyg2 
 |-  ( G e. CycGrp <-> ( G e. Grp /\ { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } =/= (/) ) )
20 3 18 19 sylanbrc 
 |-  ( ph -> G e. CycGrp )