This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid 
 |-  ( ( ( 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 )