Metamath Proof Explorer

Theorem slwhash

Description: A sylow subgroup has cardinality equal to the maximum power of P dividing the group. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypotheses fislw.1 
|- X = ( Base ` G )
slwhash.3 
|- ( ph -> X e. Fin )
slwhash.4 
|- ( ph -> H e. ( P pSyl G ) )
Assertion slwhash 
|- ( ph -> ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) )

Proof

Step Hyp Ref Expression
1 fislw.1 
 |-  X = ( Base ` G )
2 slwhash.3 
 |-  ( ph -> X e. Fin )
3 slwhash.4 
 |-  ( ph -> H e. ( P pSyl G ) )
4 slwsubg 
 |-  ( H e. ( P pSyl G ) -> H e. ( SubGrp ` G ) )
5 3 4 syl 
 |-  ( ph -> H e. ( SubGrp ` G ) )
6 subgrcl 
 |-  ( H e. ( SubGrp ` G ) -> G e. Grp )
7 5 6 syl 
 |-  ( ph -> G e. Grp )
8 slwprm 
 |-  ( H e. ( P pSyl G ) -> P e. Prime )
9 3 8 syl 
 |-  ( ph -> P e. Prime )
10 1 grpbn0 
 |-  ( G e. Grp -> X =/= (/) )
11 7 10 syl 
 |-  ( ph -> X =/= (/) )
12 hashnncl 
 |-  ( X e. Fin -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
13 2 12 syl 
 |-  ( ph -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
14 11 13 mpbird 
 |-  ( ph -> ( # ` X ) e. NN )
15 9 14 pccld 
 |-  ( ph -> ( P pCnt ( # ` X ) ) e. NN0 )
16 pcdvds 
 |-  ( ( P e. Prime /\ ( # ` X ) e. NN ) -> ( P ^ ( P pCnt ( # ` X ) ) ) || ( # ` X ) )
17 9 14 16 syl2anc 
 |-  ( ph -> ( P ^ ( P pCnt ( # ` X ) ) ) || ( # ` X ) )
18 1 7 2 9 15 17 sylow1 
 |-  ( ph -> E. k e. ( SubGrp ` G ) ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
19 2 adantr 
 |-  ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> X e. Fin )
20 5 adantr 
 |-  ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> H e. ( SubGrp ` G ) )
21 simprl 
 |-  ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> k e. ( SubGrp ` G ) )
22 eqid 
 |-  ( +g ` G ) = ( +g ` G )
23 eqid 
 |-  ( G |`s H ) = ( G |`s H )
24 23 slwpgp 
 |-  ( H e. ( P pSyl G ) -> P pGrp ( G |`s H ) )
25 3 24 syl 
 |-  ( ph -> P pGrp ( G |`s H ) )
26 25 adantr 
 |-  ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> P pGrp ( G |`s H ) )
27 simprr 
 |-  ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
28 eqid 
 |-  ( -g ` G ) = ( -g ` G )
29 1 19 20 21 22 26 27 28 sylow2b 
 |-  ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> E. g e. X H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) )
30 simprr 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) )
31 3 ad2antrr 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> H e. ( P pSyl G ) )
32 31 8 syl 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> P e. Prime )
33 15 ad2antrr 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> ( P pCnt ( # ` X ) ) e. NN0 )
34 21 adantr 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> k e. ( SubGrp ` G ) )
35 simprl 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> g e. X )
36 eqid 
 |-  ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) = ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) )
37 1 22 28 36 conjsubg 
 |-  ( ( k e. ( SubGrp ` G ) /\ g e. X ) -> ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) e. ( SubGrp ` G ) )
38 34 35 37 syl2anc 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) e. ( SubGrp ` G ) )
39 eqid 
 |-  ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) = ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) )
40 39 subgbas 
 |-  ( ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) e. ( SubGrp ` G ) -> ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) = ( Base ` ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) )
41 38 40 syl 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) = ( Base ` ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) )
42 41 fveq2d 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> ( # ` ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) = ( # ` ( Base ` ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) ) )
43 1 22 28 36 conjsubgen 
 |-  ( ( k e. ( SubGrp ` G ) /\ g e. X ) -> k ~~ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) )
44 34 35 43 syl2anc 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> k ~~ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) )
45 2 ad2antrr 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> X e. Fin )
46 1 subgss 
 |-  ( k e. ( SubGrp ` G ) -> k C_ X )
47 34 46 syl 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> k C_ X )
48 45 47 ssfid 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> k e. Fin )
49 1 subgss 
 |-  ( ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) e. ( SubGrp ` G ) -> ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) C_ X )
50 38 49 syl 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) C_ X )
51 45 50 ssfid 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) e. Fin )
52 hashen 
 |-  ( ( k e. Fin /\ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) e. Fin ) -> ( ( # ` k ) = ( # ` ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) <-> k ~~ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) )
53 48 51 52 syl2anc 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> ( ( # ` k ) = ( # ` ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) <-> k ~~ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) )
54 44 53 mpbird 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> ( # ` k ) = ( # ` ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) )
55 simplrr 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
56 54 55 eqtr3d 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> ( # ` ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
57 42 56 eqtr3d 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> ( # ` ( Base ` ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
58 oveq2 
 |-  ( n = ( P pCnt ( # ` X ) ) -> ( P ^ n ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
59 58 rspceeqv 
 |-  ( ( ( P pCnt ( # ` X ) ) e. NN0 /\ ( # ` ( Base ` ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) -> E. n e. NN0 ( # ` ( Base ` ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) ) = ( P ^ n ) )
60 33 57 59 syl2anc 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> E. n e. NN0 ( # ` ( Base ` ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) ) = ( P ^ n ) )
61 39 subggrp 
 |-  ( ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) e. ( SubGrp ` G ) -> ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) e. Grp )
62 38 61 syl 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) e. Grp )
63 41 51 eqeltrrd 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> ( Base ` ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) e. Fin )
64 eqid 
 |-  ( Base ` ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) = ( Base ` ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) )
65 64 pgpfi 
 |-  ( ( ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) e. Grp /\ ( Base ` ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) e. Fin ) -> ( P pGrp ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) <-> ( P e. Prime /\ E. n e. NN0 ( # ` ( Base ` ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) ) = ( P ^ n ) ) ) )
66 62 63 65 syl2anc 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> ( P pGrp ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) <-> ( P e. Prime /\ E. n e. NN0 ( # ` ( Base ` ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) ) = ( P ^ n ) ) ) )
67 32 60 66 mpbir2and 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> P pGrp ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) )
68 39 slwispgp 
 |-  ( ( H e. ( P pSyl G ) /\ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) e. ( SubGrp ` G ) ) -> ( ( H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) /\ P pGrp ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) <-> H = ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) )
69 31 38 68 syl2anc 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> ( ( H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) /\ P pGrp ( G |`s ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) <-> H = ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) )
70 30 67 69 mpbi2and 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> H = ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) )
71 70 fveq2d 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> ( # ` H ) = ( # ` ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) )
72 71 56 eqtrd 
 |-  ( ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) /\ ( g e. X /\ H C_ ran ( x e. k |-> ( ( g ( +g ` G ) x ) ( -g ` G ) g ) ) ) ) -> ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
73 29 72 rexlimddv 
 |-  ( ( ph /\ ( k e. ( SubGrp ` G ) /\ ( # ` k ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) -> ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
74 18 73 rexlimddv 
 |-  ( ph -> ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) )