Metamath Proof Explorer

Theorem odcau

Description: Cauchy's theorem for the order of an element in a group. A finite group whose order divides a prime P contains an element of order P . (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypotheses odcau.x 
|- X = ( Base ` G )
odcau.o 
|- O = ( od ` G )
Assertion odcau 
|- ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) -> E. g e. X ( O ` g ) = P )

Proof

Step Hyp Ref Expression
1 odcau.x 
 |-  X = ( Base ` G )
2 odcau.o 
 |-  O = ( od ` G )
3 simpl1 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) -> G e. Grp )
4 simpl2 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) -> X e. Fin )
5 simpl3 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) -> P e. Prime )
6 1nn0 
 |-  1 e. NN0
7 6 a1i 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) -> 1 e. NN0 )
8 prmnn 
 |-  ( P e. Prime -> P e. NN )
9 5 8 syl 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) -> P e. NN )
10 9 nncnd 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) -> P e. CC )
11 10 exp1d 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) -> ( P ^ 1 ) = P )
12 simpr 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) -> P || ( # ` X ) )
13 11 12 eqbrtrd 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) -> ( P ^ 1 ) || ( # ` X ) )
14 1 3 4 5 7 13 sylow1 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) -> E. s e. ( SubGrp ` G ) ( # ` s ) = ( P ^ 1 ) )
15 11 eqeq2d 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) -> ( ( # ` s ) = ( P ^ 1 ) <-> ( # ` s ) = P ) )
16 15 adantr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ s e. ( SubGrp ` G ) ) -> ( ( # ` s ) = ( P ^ 1 ) <-> ( # ` s ) = P ) )
17 fvex 
 |-  ( 0g ` G ) e. _V
18 hashsng 
 |-  ( ( 0g ` G ) e. _V -> ( # ` { ( 0g ` G ) } ) = 1 )
19 17 18 ax-mp 
 |-  ( # ` { ( 0g ` G ) } ) = 1
20 simprr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) ) -> ( # ` s ) = P )
21 5 adantr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) ) -> P e. Prime )
22 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
23 21 22 syl 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) ) -> P e. ( ZZ>= ` 2 ) )
24 20 23 eqeltrd 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) ) -> ( # ` s ) e. ( ZZ>= ` 2 ) )
25 eluz2gt1 
 |-  ( ( # ` s ) e. ( ZZ>= ` 2 ) -> 1 < ( # ` s ) )
26 24 25 syl 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) ) -> 1 < ( # ` s ) )
27 19 26 eqbrtrid 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) ) -> ( # ` { ( 0g ` G ) } ) < ( # ` s ) )
28 snfi 
 |-  { ( 0g ` G ) } e. Fin
29 4 adantr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) ) -> X e. Fin )
30 1 subgss 
 |-  ( s e. ( SubGrp ` G ) -> s C_ X )
31 30 ad2antrl 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) ) -> s C_ X )
32 29 31 ssfid 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) ) -> s e. Fin )
33 hashsdom 
 |-  ( ( { ( 0g ` G ) } e. Fin /\ s e. Fin ) -> ( ( # ` { ( 0g ` G ) } ) < ( # ` s ) <-> { ( 0g ` G ) } ~< s ) )
34 28 32 33 sylancr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) ) -> ( ( # ` { ( 0g ` G ) } ) < ( # ` s ) <-> { ( 0g ` G ) } ~< s ) )
35 27 34 mpbid 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) ) -> { ( 0g ` G ) } ~< s )
36 sdomdif 
 |-  ( { ( 0g ` G ) } ~< s -> ( s \ { ( 0g ` G ) } ) =/= (/) )
37 35 36 syl 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) ) -> ( s \ { ( 0g ` G ) } ) =/= (/) )
38 n0 
 |-  ( ( s \ { ( 0g ` G ) } ) =/= (/) <-> E. g g e. ( s \ { ( 0g ` G ) } ) )
39 37 38 sylib 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) ) -> E. g g e. ( s \ { ( 0g ` G ) } ) )
40 eldifsn 
 |-  ( g e. ( s \ { ( 0g ` G ) } ) <-> ( g e. s /\ g =/= ( 0g ` G ) ) )
41 31 adantrr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) /\ ( g e. s /\ g =/= ( 0g ` G ) ) ) ) -> s C_ X )
42 simprrl 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) /\ ( g e. s /\ g =/= ( 0g ` G ) ) ) ) -> g e. s )
43 41 42 sseldd 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) /\ ( g e. s /\ g =/= ( 0g ` G ) ) ) ) -> g e. X )
44 simprrr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) /\ ( g e. s /\ g =/= ( 0g ` G ) ) ) ) -> g =/= ( 0g ` G ) )
45 simprll 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) /\ ( g e. s /\ g =/= ( 0g ` G ) ) ) ) -> s e. ( SubGrp ` G ) )
46 32 adantrr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) /\ ( g e. s /\ g =/= ( 0g ` G ) ) ) ) -> s e. Fin )
47 2 odsubdvds 
 |-  ( ( s e. ( SubGrp ` G ) /\ s e. Fin /\ g e. s ) -> ( O ` g ) || ( # ` s ) )
48 45 46 42 47 syl3anc 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) /\ ( g e. s /\ g =/= ( 0g ` G ) ) ) ) -> ( O ` g ) || ( # ` s ) )
49 simprlr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) /\ ( g e. s /\ g =/= ( 0g ` G ) ) ) ) -> ( # ` s ) = P )
50 48 49 breqtrd 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) /\ ( g e. s /\ g =/= ( 0g ` G ) ) ) ) -> ( O ` g ) || P )
51 3 adantr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) /\ ( g e. s /\ g =/= ( 0g ` G ) ) ) ) -> G e. Grp )
52 4 adantr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) /\ ( g e. s /\ g =/= ( 0g ` G ) ) ) ) -> X e. Fin )
53 1 2 odcl2 
 |-  ( ( G e. Grp /\ X e. Fin /\ g e. X ) -> ( O ` g ) e. NN )
54 51 52 43 53 syl3anc 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) /\ ( g e. s /\ g =/= ( 0g ` G ) ) ) ) -> ( O ` g ) e. NN )
55 dvdsprime 
 |-  ( ( P e. Prime /\ ( O ` g ) e. NN ) -> ( ( O ` g ) || P <-> ( ( O ` g ) = P \/ ( O ` g ) = 1 ) ) )
56 5 54 55 syl2an2r 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) /\ ( g e. s /\ g =/= ( 0g ` G ) ) ) ) -> ( ( O ` g ) || P <-> ( ( O ` g ) = P \/ ( O ` g ) = 1 ) ) )
57 50 56 mpbid 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) /\ ( g e. s /\ g =/= ( 0g ` G ) ) ) ) -> ( ( O ` g ) = P \/ ( O ` g ) = 1 ) )
58 57 ord 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) /\ ( g e. s /\ g =/= ( 0g ` G ) ) ) ) -> ( -. ( O ` g ) = P -> ( O ` g ) = 1 ) )
59 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
60 2 59 1 odeq1 
 |-  ( ( G e. Grp /\ g e. X ) -> ( ( O ` g ) = 1 <-> g = ( 0g ` G ) ) )
61 3 43 60 syl2an2r 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) /\ ( g e. s /\ g =/= ( 0g ` G ) ) ) ) -> ( ( O ` g ) = 1 <-> g = ( 0g ` G ) ) )
62 58 61 sylibd 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) /\ ( g e. s /\ g =/= ( 0g ` G ) ) ) ) -> ( -. ( O ` g ) = P -> g = ( 0g ` G ) ) )
63 62 necon1ad 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) /\ ( g e. s /\ g =/= ( 0g ` G ) ) ) ) -> ( g =/= ( 0g ` G ) -> ( O ` g ) = P ) )
64 44 63 mpd 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) /\ ( g e. s /\ g =/= ( 0g ` G ) ) ) ) -> ( O ` g ) = P )
65 43 64 jca 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) /\ ( g e. s /\ g =/= ( 0g ` G ) ) ) ) -> ( g e. X /\ ( O ` g ) = P ) )
66 65 expr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) ) -> ( ( g e. s /\ g =/= ( 0g ` G ) ) -> ( g e. X /\ ( O ` g ) = P ) ) )
67 40 66 syl5bi 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) ) -> ( g e. ( s \ { ( 0g ` G ) } ) -> ( g e. X /\ ( O ` g ) = P ) ) )
68 67 eximdv 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) ) -> ( E. g g e. ( s \ { ( 0g ` G ) } ) -> E. g ( g e. X /\ ( O ` g ) = P ) ) )
69 39 68 mpd 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) ) -> E. g ( g e. X /\ ( O ` g ) = P ) )
70 df-rex 
 |-  ( E. g e. X ( O ` g ) = P <-> E. g ( g e. X /\ ( O ` g ) = P ) )
71 69 70 sylibr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ ( s e. ( SubGrp ` G ) /\ ( # ` s ) = P ) ) -> E. g e. X ( O ` g ) = P )
72 71 expr 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ s e. ( SubGrp ` G ) ) -> ( ( # ` s ) = P -> E. g e. X ( O ` g ) = P ) )
73 16 72 sylbid 
 |-  ( ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) /\ s e. ( SubGrp ` G ) ) -> ( ( # ` s ) = ( P ^ 1 ) -> E. g e. X ( O ` g ) = P ) )
74 73 rexlimdva 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) -> ( E. s e. ( SubGrp ` G ) ( # ` s ) = ( P ^ 1 ) -> E. g e. X ( O ` g ) = P ) )
75 14 74 mpd 
 |-  ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) -> E. g e. X ( O ` g ) = P )