Metamath Proof Explorer


Theorem sylow3lem6

Description: Lemma for sylow3 , second part. Using the lemma sylow2a , show that the number of sylow subgroups is equivalent mod P to the number of fixed points under the group action. But K is the unique element of the set of Sylow subgroups that is fixed under the group action, so there is exactly one fixed point and so ( ( #( P pSyl G ) ) mod P ) = 1 . (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 )
sylow3lem5.a
|- .+ = ( +g ` G )
sylow3lem5.d
|- .- = ( -g ` G )
sylow3lem5.k
|- ( ph -> K e. ( P pSyl G ) )
sylow3lem5.m
|- .(+) = ( x e. K , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) )
sylow3lem6.n
|- N = { x e. X | A. y e. X ( ( x .+ y ) e. s <-> ( y .+ x ) e. s ) }
Assertion sylow3lem6
|- ( ph -> ( ( # ` ( P pSyl G ) ) mod P ) = 1 )

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 sylow3lem5.a
 |-  .+ = ( +g ` G )
6 sylow3lem5.d
 |-  .- = ( -g ` G )
7 sylow3lem5.k
 |-  ( ph -> K e. ( P pSyl G ) )
8 sylow3lem5.m
 |-  .(+) = ( x e. K , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) )
9 sylow3lem6.n
 |-  N = { x e. X | A. y e. X ( ( x .+ y ) e. s <-> ( y .+ x ) e. s ) }
10 eqid
 |-  ( Base ` ( G |`s K ) ) = ( Base ` ( G |`s K ) )
11 1 2 3 4 5 6 7 8 sylow3lem5
 |-  ( ph -> .(+) e. ( ( G |`s K ) GrpAct ( P pSyl G ) ) )
12 eqid
 |-  ( G |`s K ) = ( G |`s K )
13 12 slwpgp
 |-  ( K e. ( P pSyl G ) -> P pGrp ( G |`s K ) )
14 7 13 syl
 |-  ( ph -> P pGrp ( G |`s K ) )
15 slwsubg
 |-  ( K e. ( P pSyl G ) -> K e. ( SubGrp ` G ) )
16 7 15 syl
 |-  ( ph -> K e. ( SubGrp ` G ) )
17 12 subgbas
 |-  ( K e. ( SubGrp ` G ) -> K = ( Base ` ( G |`s K ) ) )
18 16 17 syl
 |-  ( ph -> K = ( Base ` ( G |`s K ) ) )
19 1 subgss
 |-  ( K e. ( SubGrp ` G ) -> K C_ X )
20 16 19 syl
 |-  ( ph -> K C_ X )
21 3 20 ssfid
 |-  ( ph -> K e. Fin )
22 18 21 eqeltrrd
 |-  ( ph -> ( Base ` ( G |`s K ) ) e. Fin )
23 pwfi
 |-  ( X e. Fin <-> ~P X e. Fin )
24 3 23 sylib
 |-  ( ph -> ~P X e. Fin )
25 slwsubg
 |-  ( x e. ( P pSyl G ) -> x e. ( SubGrp ` G ) )
26 1 subgss
 |-  ( x e. ( SubGrp ` G ) -> x C_ X )
27 25 26 syl
 |-  ( x e. ( P pSyl G ) -> x C_ X )
28 25 27 elpwd
 |-  ( x e. ( P pSyl G ) -> x e. ~P X )
29 28 ssriv
 |-  ( P pSyl G ) C_ ~P X
30 ssfi
 |-  ( ( ~P X e. Fin /\ ( P pSyl G ) C_ ~P X ) -> ( P pSyl G ) e. Fin )
31 24 29 30 sylancl
 |-  ( ph -> ( P pSyl G ) e. Fin )
32 eqid
 |-  { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } = { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s }
33 eqid
 |-  { <. z , w >. | ( { z , w } C_ ( P pSyl G ) /\ E. h e. ( Base ` ( G |`s K ) ) ( h .(+) z ) = w ) } = { <. z , w >. | ( { z , w } C_ ( P pSyl G ) /\ E. h e. ( Base ` ( G |`s K ) ) ( h .(+) z ) = w ) }
34 10 11 14 22 31 32 33 sylow2a
 |-  ( ph -> P || ( ( # ` ( P pSyl G ) ) - ( # ` { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } ) ) )
35 eqcom
 |-  ( ran ( z e. s |-> ( ( g .+ z ) .- g ) ) = s <-> s = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) )
36 20 adantr
 |-  ( ( ph /\ s e. ( P pSyl G ) ) -> K C_ X )
37 36 sselda
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> g e. X )
38 37 biantrurd
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> ( s = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) <-> ( g e. X /\ s = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) ) ) )
39 35 38 syl5bb
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> ( ran ( z e. s |-> ( ( g .+ z ) .- g ) ) = s <-> ( g e. X /\ s = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) ) ) )
40 simpr
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> g e. K )
41 simplr
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> s e. ( P pSyl G ) )
42 simpr
 |-  ( ( x = g /\ y = s ) -> y = s )
43 simpl
 |-  ( ( x = g /\ y = s ) -> x = g )
44 43 oveq1d
 |-  ( ( x = g /\ y = s ) -> ( x .+ z ) = ( g .+ z ) )
45 44 43 oveq12d
 |-  ( ( x = g /\ y = s ) -> ( ( x .+ z ) .- x ) = ( ( g .+ z ) .- g ) )
46 42 45 mpteq12dv
 |-  ( ( x = g /\ y = s ) -> ( z e. y |-> ( ( x .+ z ) .- x ) ) = ( z e. s |-> ( ( g .+ z ) .- g ) ) )
47 46 rneqd
 |-  ( ( x = g /\ y = s ) -> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) )
48 vex
 |-  s e. _V
49 48 mptex
 |-  ( z e. s |-> ( ( g .+ z ) .- g ) ) e. _V
50 49 rnex
 |-  ran ( z e. s |-> ( ( g .+ z ) .- g ) ) e. _V
51 47 8 50 ovmpoa
 |-  ( ( g e. K /\ s e. ( P pSyl G ) ) -> ( g .(+) s ) = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) )
52 40 41 51 syl2anc
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> ( g .(+) s ) = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) )
53 52 eqeq1d
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> ( ( g .(+) s ) = s <-> ran ( z e. s |-> ( ( g .+ z ) .- g ) ) = s ) )
54 slwsubg
 |-  ( s e. ( P pSyl G ) -> s e. ( SubGrp ` G ) )
55 54 ad2antlr
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> s e. ( SubGrp ` G ) )
56 eqid
 |-  ( z e. s |-> ( ( g .+ z ) .- g ) ) = ( z e. s |-> ( ( g .+ z ) .- g ) )
57 1 5 6 56 9 conjnmzb
 |-  ( s e. ( SubGrp ` G ) -> ( g e. N <-> ( g e. X /\ s = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) ) ) )
58 55 57 syl
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> ( g e. N <-> ( g e. X /\ s = ran ( z e. s |-> ( ( g .+ z ) .- g ) ) ) ) )
59 39 53 58 3bitr4d
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ g e. K ) -> ( ( g .(+) s ) = s <-> g e. N ) )
60 59 ralbidva
 |-  ( ( ph /\ s e. ( P pSyl G ) ) -> ( A. g e. K ( g .(+) s ) = s <-> A. g e. K g e. N ) )
61 dfss3
 |-  ( K C_ N <-> A. g e. K g e. N )
62 60 61 bitr4di
 |-  ( ( ph /\ s e. ( P pSyl G ) ) -> ( A. g e. K ( g .(+) s ) = s <-> K C_ N ) )
63 18 adantr
 |-  ( ( ph /\ s e. ( P pSyl G ) ) -> K = ( Base ` ( G |`s K ) ) )
64 63 raleqdv
 |-  ( ( ph /\ s e. ( P pSyl G ) ) -> ( A. g e. K ( g .(+) s ) = s <-> A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s ) )
65 eqid
 |-  ( Base ` ( G |`s N ) ) = ( Base ` ( G |`s N ) )
66 2 ad2antrr
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> G e. Grp )
67 9 1 5 nmzsubg
 |-  ( G e. Grp -> N e. ( SubGrp ` G ) )
68 66 67 syl
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> N e. ( SubGrp ` G ) )
69 eqid
 |-  ( G |`s N ) = ( G |`s N )
70 69 subgbas
 |-  ( N e. ( SubGrp ` G ) -> N = ( Base ` ( G |`s N ) ) )
71 68 70 syl
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> N = ( Base ` ( G |`s N ) ) )
72 3 ad2antrr
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> X e. Fin )
73 1 subgss
 |-  ( N e. ( SubGrp ` G ) -> N C_ X )
74 68 73 syl
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> N C_ X )
75 72 74 ssfid
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> N e. Fin )
76 71 75 eqeltrrd
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> ( Base ` ( G |`s N ) ) e. Fin )
77 7 ad2antrr
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> K e. ( P pSyl G ) )
78 simpr
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> K C_ N )
79 69 subgslw
 |-  ( ( N e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ N ) -> K e. ( P pSyl ( G |`s N ) ) )
80 68 77 78 79 syl3anc
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> K e. ( P pSyl ( G |`s N ) ) )
81 simplr
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> s e. ( P pSyl G ) )
82 54 ad2antlr
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> s e. ( SubGrp ` G ) )
83 9 1 5 ssnmz
 |-  ( s e. ( SubGrp ` G ) -> s C_ N )
84 82 83 syl
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> s C_ N )
85 69 subgslw
 |-  ( ( N e. ( SubGrp ` G ) /\ s e. ( P pSyl G ) /\ s C_ N ) -> s e. ( P pSyl ( G |`s N ) ) )
86 68 81 84 85 syl3anc
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> s e. ( P pSyl ( G |`s N ) ) )
87 1 fvexi
 |-  X e. _V
88 9 87 rabex2
 |-  N e. _V
89 69 5 ressplusg
 |-  ( N e. _V -> .+ = ( +g ` ( G |`s N ) ) )
90 88 89 ax-mp
 |-  .+ = ( +g ` ( G |`s N ) )
91 eqid
 |-  ( -g ` ( G |`s N ) ) = ( -g ` ( G |`s N ) )
92 65 76 80 86 90 91 sylow2
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> E. g e. ( Base ` ( G |`s N ) ) K = ran ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) )
93 9 1 5 69 nmznsg
 |-  ( s e. ( SubGrp ` G ) -> s e. ( NrmSGrp ` ( G |`s N ) ) )
94 82 93 syl
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> s e. ( NrmSGrp ` ( G |`s N ) ) )
95 eqid
 |-  ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) = ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) )
96 65 90 91 95 conjnsg
 |-  ( ( s e. ( NrmSGrp ` ( G |`s N ) ) /\ g e. ( Base ` ( G |`s N ) ) ) -> s = ran ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) )
97 94 96 sylan
 |-  ( ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) /\ g e. ( Base ` ( G |`s N ) ) ) -> s = ran ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) )
98 eqeq2
 |-  ( K = ran ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) -> ( s = K <-> s = ran ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) ) )
99 97 98 syl5ibrcom
 |-  ( ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) /\ g e. ( Base ` ( G |`s N ) ) ) -> ( K = ran ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) -> s = K ) )
100 99 rexlimdva
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> ( E. g e. ( Base ` ( G |`s N ) ) K = ran ( z e. s |-> ( ( g .+ z ) ( -g ` ( G |`s N ) ) g ) ) -> s = K ) )
101 92 100 mpd
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ K C_ N ) -> s = K )
102 simpr
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ s = K ) -> s = K )
103 16 ad2antrr
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ s = K ) -> K e. ( SubGrp ` G ) )
104 102 103 eqeltrd
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ s = K ) -> s e. ( SubGrp ` G ) )
105 104 83 syl
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ s = K ) -> s C_ N )
106 102 105 eqsstrrd
 |-  ( ( ( ph /\ s e. ( P pSyl G ) ) /\ s = K ) -> K C_ N )
107 101 106 impbida
 |-  ( ( ph /\ s e. ( P pSyl G ) ) -> ( K C_ N <-> s = K ) )
108 62 64 107 3bitr3d
 |-  ( ( ph /\ s e. ( P pSyl G ) ) -> ( A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s <-> s = K ) )
109 108 rabbidva
 |-  ( ph -> { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } = { s e. ( P pSyl G ) | s = K } )
110 rabsn
 |-  ( K e. ( P pSyl G ) -> { s e. ( P pSyl G ) | s = K } = { K } )
111 7 110 syl
 |-  ( ph -> { s e. ( P pSyl G ) | s = K } = { K } )
112 109 111 eqtrd
 |-  ( ph -> { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } = { K } )
113 112 fveq2d
 |-  ( ph -> ( # ` { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } ) = ( # ` { K } ) )
114 hashsng
 |-  ( K e. ( P pSyl G ) -> ( # ` { K } ) = 1 )
115 7 114 syl
 |-  ( ph -> ( # ` { K } ) = 1 )
116 113 115 eqtrd
 |-  ( ph -> ( # ` { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } ) = 1 )
117 116 oveq2d
 |-  ( ph -> ( ( # ` ( P pSyl G ) ) - ( # ` { s e. ( P pSyl G ) | A. g e. ( Base ` ( G |`s K ) ) ( g .(+) s ) = s } ) ) = ( ( # ` ( P pSyl G ) ) - 1 ) )
118 34 117 breqtrd
 |-  ( ph -> P || ( ( # ` ( P pSyl G ) ) - 1 ) )
119 prmnn
 |-  ( P e. Prime -> P e. NN )
120 4 119 syl
 |-  ( ph -> P e. NN )
121 hashcl
 |-  ( ( P pSyl G ) e. Fin -> ( # ` ( P pSyl G ) ) e. NN0 )
122 31 121 syl
 |-  ( ph -> ( # ` ( P pSyl G ) ) e. NN0 )
123 122 nn0zd
 |-  ( ph -> ( # ` ( P pSyl G ) ) e. ZZ )
124 1zzd
 |-  ( ph -> 1 e. ZZ )
125 moddvds
 |-  ( ( P e. NN /\ ( # ` ( P pSyl G ) ) e. ZZ /\ 1 e. ZZ ) -> ( ( ( # ` ( P pSyl G ) ) mod P ) = ( 1 mod P ) <-> P || ( ( # ` ( P pSyl G ) ) - 1 ) ) )
126 120 123 124 125 syl3anc
 |-  ( ph -> ( ( ( # ` ( P pSyl G ) ) mod P ) = ( 1 mod P ) <-> P || ( ( # ` ( P pSyl G ) ) - 1 ) ) )
127 118 126 mpbird
 |-  ( ph -> ( ( # ` ( P pSyl G ) ) mod P ) = ( 1 mod P ) )
128 prmuz2
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
129 eluz2b2
 |-  ( P e. ( ZZ>= ` 2 ) <-> ( P e. NN /\ 1 < P ) )
130 nnre
 |-  ( P e. NN -> P e. RR )
131 1mod
 |-  ( ( P e. RR /\ 1 < P ) -> ( 1 mod P ) = 1 )
132 130 131 sylan
 |-  ( ( P e. NN /\ 1 < P ) -> ( 1 mod P ) = 1 )
133 129 132 sylbi
 |-  ( P e. ( ZZ>= ` 2 ) -> ( 1 mod P ) = 1 )
134 4 128 133 3syl
 |-  ( ph -> ( 1 mod P ) = 1 )
135 127 134 eqtrd
 |-  ( ph -> ( ( # ` ( P pSyl G ) ) mod P ) = 1 )