Metamath Proof Explorer

Theorem sylow3lem4

Description: Lemma for sylow3 , first part. The number of Sylow subgroups is a divisor of the size of G reduced by the size of a Sylow subgroup of G . (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypotheses sylow3.x 
|- X = ( Base ` G )
sylow3.g 
|- ( ph -> G e. Grp )
sylow3.xf 
|- ( ph -> X e. Fin )
sylow3.p 
|- ( ph -> P e. Prime )
sylow3lem1.a 
|- .+ = ( +g ` G )
sylow3lem1.d 
|- .- = ( -g ` G )
sylow3lem1.m 
|- .(+) = ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) )
sylow3lem2.k 
|- ( ph -> K e. ( P pSyl G ) )
sylow3lem2.h 
|- H = { u e. X | ( u .(+) K ) = K }
sylow3lem2.n 
|- N = { x e. X | A. y e. X ( ( x .+ y ) e. K <-> ( y .+ x ) e. K ) }
Assertion sylow3lem4 
|- ( ph -> ( # ` ( P pSyl G ) ) || ( ( # ` X ) / ( P ^ ( P pCnt ( # ` X ) ) ) ) )

Proof

Step Hyp Ref Expression
1 sylow3.x 
 |-  X = ( Base ` G )
2 sylow3.g 
 |-  ( ph -> G e. Grp )
3 sylow3.xf 
 |-  ( ph -> X e. Fin )
4 sylow3.p 
 |-  ( ph -> P e. Prime )
5 sylow3lem1.a 
 |-  .+ = ( +g ` G )
6 sylow3lem1.d 
 |-  .- = ( -g ` G )
7 sylow3lem1.m 
 |-  .(+) = ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) )
8 sylow3lem2.k 
 |-  ( ph -> K e. ( P pSyl G ) )
9 sylow3lem2.h 
 |-  H = { u e. X | ( u .(+) K ) = K }
10 sylow3lem2.n 
 |-  N = { x e. X | A. y e. X ( ( x .+ y ) e. K <-> ( y .+ x ) e. K ) }
11 1 2 3 4 5 6 7 8 9 10 sylow3lem3 
 |-  ( ph -> ( # ` ( P pSyl G ) ) = ( # ` ( X /. ( G ~QG N ) ) ) )
12 slwsubg 
 |-  ( K e. ( P pSyl G ) -> K e. ( SubGrp ` G ) )
13 8 12 syl 
 |-  ( ph -> K e. ( SubGrp ` G ) )
14 eqid 
 |-  ( G |`s N ) = ( G |`s N )
15 10 1 5 14 nmznsg 
 |-  ( K e. ( SubGrp ` G ) -> K e. ( NrmSGrp ` ( G |`s N ) ) )
16 nsgsubg 
 |-  ( K e. ( NrmSGrp ` ( G |`s N ) ) -> K e. ( SubGrp ` ( G |`s N ) ) )
17 15 16 syl 
 |-  ( K e. ( SubGrp ` G ) -> K e. ( SubGrp ` ( G |`s N ) ) )
18 13 17 syl 
 |-  ( ph -> K e. ( SubGrp ` ( G |`s N ) ) )
19 10 1 5 nmzsubg 
 |-  ( G e. Grp -> N e. ( SubGrp ` G ) )
20 2 19 syl 
 |-  ( ph -> N e. ( SubGrp ` G ) )
21 14 subgbas 
 |-  ( N e. ( SubGrp ` G ) -> N = ( Base ` ( G |`s N ) ) )
22 20 21 syl 
 |-  ( ph -> N = ( Base ` ( G |`s N ) ) )
23 1 subgss 
 |-  ( N e. ( SubGrp ` G ) -> N C_ X )
24 20 23 syl 
 |-  ( ph -> N C_ X )
25 3 24 ssfid 
 |-  ( ph -> N e. Fin )
26 22 25 eqeltrrd 
 |-  ( ph -> ( Base ` ( G |`s N ) ) e. Fin )
27 eqid 
 |-  ( Base ` ( G |`s N ) ) = ( Base ` ( G |`s N ) )
28 27 lagsubg 
 |-  ( ( K e. ( SubGrp ` ( G |`s N ) ) /\ ( Base ` ( G |`s N ) ) e. Fin ) -> ( # ` K ) || ( # ` ( Base ` ( G |`s N ) ) ) )
29 18 26 28 syl2anc 
 |-  ( ph -> ( # ` K ) || ( # ` ( Base ` ( G |`s N ) ) ) )
30 22 fveq2d 
 |-  ( ph -> ( # ` N ) = ( # ` ( Base ` ( G |`s N ) ) ) )
31 29 30 breqtrrd 
 |-  ( ph -> ( # ` K ) || ( # ` N ) )
32 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
33 32 subg0cl 
 |-  ( K e. ( SubGrp ` G ) -> ( 0g ` G ) e. K )
34 13 33 syl 
 |-  ( ph -> ( 0g ` G ) e. K )
35 34 ne0d 
 |-  ( ph -> K =/= (/) )
36 1 subgss 
 |-  ( K e. ( SubGrp ` G ) -> K C_ X )
37 13 36 syl 
 |-  ( ph -> K C_ X )
38 3 37 ssfid 
 |-  ( ph -> K e. Fin )
39 hashnncl 
 |-  ( K e. Fin -> ( ( # ` K ) e. NN <-> K =/= (/) ) )
40 38 39 syl 
 |-  ( ph -> ( ( # ` K ) e. NN <-> K =/= (/) ) )
41 35 40 mpbird 
 |-  ( ph -> ( # ` K ) e. NN )
42 41 nnzd 
 |-  ( ph -> ( # ` K ) e. ZZ )
43 hashcl 
 |-  ( N e. Fin -> ( # ` N ) e. NN0 )
44 25 43 syl 
 |-  ( ph -> ( # ` N ) e. NN0 )
45 44 nn0zd 
 |-  ( ph -> ( # ` N ) e. ZZ )
46 pwfi 
 |-  ( X e. Fin <-> ~P X e. Fin )
47 3 46 sylib 
 |-  ( ph -> ~P X e. Fin )
48 eqid 
 |-  ( G ~QG N ) = ( G ~QG N )
49 1 48 eqger 
 |-  ( N e. ( SubGrp ` G ) -> ( G ~QG N ) Er X )
50 20 49 syl 
 |-  ( ph -> ( G ~QG N ) Er X )
51 50 qsss 
 |-  ( ph -> ( X /. ( G ~QG N ) ) C_ ~P X )
52 47 51 ssfid 
 |-  ( ph -> ( X /. ( G ~QG N ) ) e. Fin )
53 hashcl 
 |-  ( ( X /. ( G ~QG N ) ) e. Fin -> ( # ` ( X /. ( G ~QG N ) ) ) e. NN0 )
54 52 53 syl 
 |-  ( ph -> ( # ` ( X /. ( G ~QG N ) ) ) e. NN0 )
55 54 nn0zd 
 |-  ( ph -> ( # ` ( X /. ( G ~QG N ) ) ) e. ZZ )
56 dvdscmul 
 |-  ( ( ( # ` K ) e. ZZ /\ ( # ` N ) e. ZZ /\ ( # ` ( X /. ( G ~QG N ) ) ) e. ZZ ) -> ( ( # ` K ) || ( # ` N ) -> ( ( # ` ( X /. ( G ~QG N ) ) ) x. ( # ` K ) ) || ( ( # ` ( X /. ( G ~QG N ) ) ) x. ( # ` N ) ) ) )
57 42 45 55 56 syl3anc 
 |-  ( ph -> ( ( # ` K ) || ( # ` N ) -> ( ( # ` ( X /. ( G ~QG N ) ) ) x. ( # ` K ) ) || ( ( # ` ( X /. ( G ~QG N ) ) ) x. ( # ` N ) ) ) )
58 31 57 mpd 
 |-  ( ph -> ( ( # ` ( X /. ( G ~QG N ) ) ) x. ( # ` K ) ) || ( ( # ` ( X /. ( G ~QG N ) ) ) x. ( # ` N ) ) )
59 hashcl 
 |-  ( X e. Fin -> ( # ` X ) e. NN0 )
60 3 59 syl 
 |-  ( ph -> ( # ` X ) e. NN0 )
61 60 nn0cnd 
 |-  ( ph -> ( # ` X ) e. CC )
62 41 nncnd 
 |-  ( ph -> ( # ` K ) e. CC )
63 41 nnne0d 
 |-  ( ph -> ( # ` K ) =/= 0 )
64 61 62 63 divcan1d 
 |-  ( ph -> ( ( ( # ` X ) / ( # ` K ) ) x. ( # ` K ) ) = ( # ` X ) )
65 1 48 20 3 lagsubg2 
 |-  ( ph -> ( # ` X ) = ( ( # ` ( X /. ( G ~QG N ) ) ) x. ( # ` N ) ) )
66 64 65 eqtrd 
 |-  ( ph -> ( ( ( # ` X ) / ( # ` K ) ) x. ( # ` K ) ) = ( ( # ` ( X /. ( G ~QG N ) ) ) x. ( # ` N ) ) )
67 58 66 breqtrrd 
 |-  ( ph -> ( ( # ` ( X /. ( G ~QG N ) ) ) x. ( # ` K ) ) || ( ( ( # ` X ) / ( # ` K ) ) x. ( # ` K ) ) )
68 1 lagsubg 
 |-  ( ( K e. ( SubGrp ` G ) /\ X e. Fin ) -> ( # ` K ) || ( # ` X ) )
69 13 3 68 syl2anc 
 |-  ( ph -> ( # ` K ) || ( # ` X ) )
70 60 nn0zd 
 |-  ( ph -> ( # ` X ) e. ZZ )
71 dvdsval2 
 |-  ( ( ( # ` K ) e. ZZ /\ ( # ` K ) =/= 0 /\ ( # ` X ) e. ZZ ) -> ( ( # ` K ) || ( # ` X ) <-> ( ( # ` X ) / ( # ` K ) ) e. ZZ ) )
72 42 63 70 71 syl3anc 
 |-  ( ph -> ( ( # ` K ) || ( # ` X ) <-> ( ( # ` X ) / ( # ` K ) ) e. ZZ ) )
73 69 72 mpbid 
 |-  ( ph -> ( ( # ` X ) / ( # ` K ) ) e. ZZ )
74 dvdsmulcr 
 |-  ( ( ( # ` ( X /. ( G ~QG N ) ) ) e. ZZ /\ ( ( # ` X ) / ( # ` K ) ) e. ZZ /\ ( ( # ` K ) e. ZZ /\ ( # ` K ) =/= 0 ) ) -> ( ( ( # ` ( X /. ( G ~QG N ) ) ) x. ( # ` K ) ) || ( ( ( # ` X ) / ( # ` K ) ) x. ( # ` K ) ) <-> ( # ` ( X /. ( G ~QG N ) ) ) || ( ( # ` X ) / ( # ` K ) ) ) )
75 55 73 42 63 74 syl112anc 
 |-  ( ph -> ( ( ( # ` ( X /. ( G ~QG N ) ) ) x. ( # ` K ) ) || ( ( ( # ` X ) / ( # ` K ) ) x. ( # ` K ) ) <-> ( # ` ( X /. ( G ~QG N ) ) ) || ( ( # ` X ) / ( # ` K ) ) ) )
76 67 75 mpbid 
 |-  ( ph -> ( # ` ( X /. ( G ~QG N ) ) ) || ( ( # ` X ) / ( # ` K ) ) )
77 1 3 8 slwhash 
 |-  ( ph -> ( # ` K ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
78 77 oveq2d 
 |-  ( ph -> ( ( # ` X ) / ( # ` K ) ) = ( ( # ` X ) / ( P ^ ( P pCnt ( # ` X ) ) ) ) )
79 76 78 breqtrd 
 |-  ( ph -> ( # ` ( X /. ( G ~QG N ) ) ) || ( ( # ` X ) / ( P ^ ( P pCnt ( # ` X ) ) ) ) )
80 11 79 eqbrtrd 
 |-  ( ph -> ( # ` ( P pSyl G ) ) || ( ( # ` X ) / ( P ^ ( P pCnt ( # ` X ) ) ) ) )