Metamath Proof Explorer

Theorem prmcyg

Description: A group with prime order is cyclic. (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Hypothesis cygctb.1 
|- B = ( Base ` G )
Assertion prmcyg 
|- ( ( G e. Grp /\ ( # ` B ) e. Prime ) -> G e. CycGrp )

Proof

Step Hyp Ref Expression
1 cygctb.1 
 |-  B = ( Base ` G )
2 1nprm 
 |-  -. 1 e. Prime
3 simpr 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ B C_ { ( 0g ` G ) } ) -> B C_ { ( 0g ` G ) } )
4 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
5 1 4 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. B )
6 5 snssd 
 |-  ( G e. Grp -> { ( 0g ` G ) } C_ B )
7 6 ad2antrr 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ B C_ { ( 0g ` G ) } ) -> { ( 0g ` G ) } C_ B )
8 3 7 eqssd 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ B C_ { ( 0g ` G ) } ) -> B = { ( 0g ` G ) } )
9 8 fveq2d 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ B C_ { ( 0g ` G ) } ) -> ( # ` B ) = ( # ` { ( 0g ` G ) } ) )
10 fvex 
 |-  ( 0g ` G ) e. _V
11 hashsng 
 |-  ( ( 0g ` G ) e. _V -> ( # ` { ( 0g ` G ) } ) = 1 )
12 10 11 ax-mp 
 |-  ( # ` { ( 0g ` G ) } ) = 1
13 9 12 eqtrdi 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ B C_ { ( 0g ` G ) } ) -> ( # ` B ) = 1 )
14 simplr 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ B C_ { ( 0g ` G ) } ) -> ( # ` B ) e. Prime )
15 13 14 eqeltrrd 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ B C_ { ( 0g ` G ) } ) -> 1 e. Prime )
16 15 ex 
 |-  ( ( G e. Grp /\ ( # ` B ) e. Prime ) -> ( B C_ { ( 0g ` G ) } -> 1 e. Prime ) )
17 2 16 mtoi 
 |-  ( ( G e. Grp /\ ( # ` B ) e. Prime ) -> -. B C_ { ( 0g ` G ) } )
18 nss 
 |-  ( -. B C_ { ( 0g ` G ) } <-> E. x ( x e. B /\ -. x e. { ( 0g ` G ) } ) )
19 17 18 sylib 
 |-  ( ( G e. Grp /\ ( # ` B ) e. Prime ) -> E. x ( x e. B /\ -. x e. { ( 0g ` G ) } ) )
20 eqid 
 |-  ( od ` G ) = ( od ` G )
21 simpll 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ ( x e. B /\ -. x e. { ( 0g ` G ) } ) ) -> G e. Grp )
22 simprl 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ ( x e. B /\ -. x e. { ( 0g ` G ) } ) ) -> x e. B )
23 simprr 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ ( x e. B /\ -. x e. { ( 0g ` G ) } ) ) -> -. x e. { ( 0g ` G ) } )
24 20 4 1 odeq1 
 |-  ( ( G e. Grp /\ x e. B ) -> ( ( ( od ` G ) ` x ) = 1 <-> x = ( 0g ` G ) ) )
25 21 22 24 syl2anc 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ ( x e. B /\ -. x e. { ( 0g ` G ) } ) ) -> ( ( ( od ` G ) ` x ) = 1 <-> x = ( 0g ` G ) ) )
26 velsn 
 |-  ( x e. { ( 0g ` G ) } <-> x = ( 0g ` G ) )
27 25 26 bitr4di 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ ( x e. B /\ -. x e. { ( 0g ` G ) } ) ) -> ( ( ( od ` G ) ` x ) = 1 <-> x e. { ( 0g ` G ) } ) )
28 23 27 mtbird 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ ( x e. B /\ -. x e. { ( 0g ` G ) } ) ) -> -. ( ( od ` G ) ` x ) = 1 )
29 prmnn 
 |-  ( ( # ` B ) e. Prime -> ( # ` B ) e. NN )
30 29 ad2antlr 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ ( x e. B /\ -. x e. { ( 0g ` G ) } ) ) -> ( # ` B ) e. NN )
31 30 nnnn0d 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ ( x e. B /\ -. x e. { ( 0g ` G ) } ) ) -> ( # ` B ) e. NN0 )
32 1 fvexi 
 |-  B e. _V
33 hashclb 
 |-  ( B e. _V -> ( B e. Fin <-> ( # ` B ) e. NN0 ) )
34 32 33 ax-mp 
 |-  ( B e. Fin <-> ( # ` B ) e. NN0 )
35 31 34 sylibr 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ ( x e. B /\ -. x e. { ( 0g ` G ) } ) ) -> B e. Fin )
36 1 20 oddvds2 
 |-  ( ( G e. Grp /\ B e. Fin /\ x e. B ) -> ( ( od ` G ) ` x ) || ( # ` B ) )
37 21 35 22 36 syl3anc 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ ( x e. B /\ -. x e. { ( 0g ` G ) } ) ) -> ( ( od ` G ) ` x ) || ( # ` B ) )
38 simplr 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ ( x e. B /\ -. x e. { ( 0g ` G ) } ) ) -> ( # ` B ) e. Prime )
39 1 20 odcl2 
 |-  ( ( G e. Grp /\ B e. Fin /\ x e. B ) -> ( ( od ` G ) ` x ) e. NN )
40 21 35 22 39 syl3anc 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ ( x e. B /\ -. x e. { ( 0g ` G ) } ) ) -> ( ( od ` G ) ` x ) e. NN )
41 dvdsprime 
 |-  ( ( ( # ` B ) e. Prime /\ ( ( od ` G ) ` x ) e. NN ) -> ( ( ( od ` G ) ` x ) || ( # ` B ) <-> ( ( ( od ` G ) ` x ) = ( # ` B ) \/ ( ( od ` G ) ` x ) = 1 ) ) )
42 38 40 41 syl2anc 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ ( x e. B /\ -. x e. { ( 0g ` G ) } ) ) -> ( ( ( od ` G ) ` x ) || ( # ` B ) <-> ( ( ( od ` G ) ` x ) = ( # ` B ) \/ ( ( od ` G ) ` x ) = 1 ) ) )
43 37 42 mpbid 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ ( x e. B /\ -. x e. { ( 0g ` G ) } ) ) -> ( ( ( od ` G ) ` x ) = ( # ` B ) \/ ( ( od ` G ) ` x ) = 1 ) )
44 43 ord 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ ( x e. B /\ -. x e. { ( 0g ` G ) } ) ) -> ( -. ( ( od ` G ) ` x ) = ( # ` B ) -> ( ( od ` G ) ` x ) = 1 ) )
45 28 44 mt3d 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ ( x e. B /\ -. x e. { ( 0g ` G ) } ) ) -> ( ( od ` G ) ` x ) = ( # ` B ) )
46 1 20 21 22 45 iscygodd 
 |-  ( ( ( G e. Grp /\ ( # ` B ) e. Prime ) /\ ( x e. B /\ -. x e. { ( 0g ` G ) } ) ) -> G e. CycGrp )
47 19 46 exlimddv 
 |-  ( ( G e. Grp /\ ( # ` B ) e. Prime ) -> G e. CycGrp )