Metamath Proof Explorer

Theorem sylow2alem2

Description: Lemma for sylow2a . All the orbits which are not for fixed points have size | G | / | G x | (where G x is the stabilizer subgroup) and thus are powers of P . And since they are all nontrivial (because any orbit which is a singleton is a fixed point), they all divide P , and so does the sum of all of them. (Contributed by Mario Carneiro, 17-Jan-2015)

Ref Expression
Hypotheses sylow2a.x 
|- X = ( Base ` G )
sylow2a.m 
|- ( ph -> .(+) e. ( G GrpAct Y ) )
sylow2a.p 
|- ( ph -> P pGrp G )
sylow2a.f 
|- ( ph -> X e. Fin )
sylow2a.y 
|- ( ph -> Y e. Fin )
sylow2a.z 
|- Z = { u e. Y | A. h e. X ( h .(+) u ) = u }
sylow2a.r 
|- .~ = { <. x , y >. | ( { x , y } C_ Y /\ E. g e. X ( g .(+) x ) = y ) }
Assertion sylow2alem2 
|- ( ph -> P || sum_ z e. ( ( Y /. .~ ) \ ~P Z ) ( # ` z ) )

Proof

Step Hyp Ref Expression
1 sylow2a.x 
 |-  X = ( Base ` G )
2 sylow2a.m 
 |-  ( ph -> .(+) e. ( G GrpAct Y ) )
3 sylow2a.p 
 |-  ( ph -> P pGrp G )
4 sylow2a.f 
 |-  ( ph -> X e. Fin )
5 sylow2a.y 
 |-  ( ph -> Y e. Fin )
6 sylow2a.z 
 |-  Z = { u e. Y | A. h e. X ( h .(+) u ) = u }
7 sylow2a.r 
 |-  .~ = { <. x , y >. | ( { x , y } C_ Y /\ E. g e. X ( g .(+) x ) = y ) }
8 pwfi 
 |-  ( Y e. Fin <-> ~P Y e. Fin )
9 5 8 sylib 
 |-  ( ph -> ~P Y e. Fin )
10 7 1 gaorber 
 |-  ( .(+) e. ( G GrpAct Y ) -> .~ Er Y )
11 2 10 syl 
 |-  ( ph -> .~ Er Y )
12 11 qsss 
 |-  ( ph -> ( Y /. .~ ) C_ ~P Y )
13 9 12 ssfid 
 |-  ( ph -> ( Y /. .~ ) e. Fin )
14 diffi 
 |-  ( ( Y /. .~ ) e. Fin -> ( ( Y /. .~ ) \ ~P Z ) e. Fin )
15 13 14 syl 
 |-  ( ph -> ( ( Y /. .~ ) \ ~P Z ) e. Fin )
16 gagrp 
 |-  ( .(+) e. ( G GrpAct Y ) -> G e. Grp )
17 2 16 syl 
 |-  ( ph -> G e. Grp )
18 1 pgpfi 
 |-  ( ( G e. Grp /\ X e. Fin ) -> ( P pGrp G <-> ( P e. Prime /\ E. n e. NN0 ( # ` X ) = ( P ^ n ) ) ) )
19 17 4 18 syl2anc 
 |-  ( ph -> ( P pGrp G <-> ( P e. Prime /\ E. n e. NN0 ( # ` X ) = ( P ^ n ) ) ) )
20 3 19 mpbid 
 |-  ( ph -> ( P e. Prime /\ E. n e. NN0 ( # ` X ) = ( P ^ n ) ) )
21 20 simpld 
 |-  ( ph -> P e. Prime )
22 prmz 
 |-  ( P e. Prime -> P e. ZZ )
23 21 22 syl 
 |-  ( ph -> P e. ZZ )
24 eldifi 
 |-  ( z e. ( ( Y /. .~ ) \ ~P Z ) -> z e. ( Y /. .~ ) )
25 5 adantr 
 |-  ( ( ph /\ z e. ( Y /. .~ ) ) -> Y e. Fin )
26 12 sselda 
 |-  ( ( ph /\ z e. ( Y /. .~ ) ) -> z e. ~P Y )
27 26 elpwid 
 |-  ( ( ph /\ z e. ( Y /. .~ ) ) -> z C_ Y )
28 25 27 ssfid 
 |-  ( ( ph /\ z e. ( Y /. .~ ) ) -> z e. Fin )
29 24 28 sylan2 
 |-  ( ( ph /\ z e. ( ( Y /. .~ ) \ ~P Z ) ) -> z e. Fin )
30 hashcl 
 |-  ( z e. Fin -> ( # ` z ) e. NN0 )
31 29 30 syl 
 |-  ( ( ph /\ z e. ( ( Y /. .~ ) \ ~P Z ) ) -> ( # ` z ) e. NN0 )
32 31 nn0zd 
 |-  ( ( ph /\ z e. ( ( Y /. .~ ) \ ~P Z ) ) -> ( # ` z ) e. ZZ )
33 eldif 
 |-  ( z e. ( ( Y /. .~ ) \ ~P Z ) <-> ( z e. ( Y /. .~ ) /\ -. z e. ~P Z ) )
34 eqid 
 |-  ( Y /. .~ ) = ( Y /. .~ )
35 sseq1 
 |-  ( [ w ] .~ = z -> ( [ w ] .~ C_ Z <-> z C_ Z ) )
36 velpw 
 |-  ( z e. ~P Z <-> z C_ Z )
37 35 36 bitr4di 
 |-  ( [ w ] .~ = z -> ( [ w ] .~ C_ Z <-> z e. ~P Z ) )
38 37 notbid 
 |-  ( [ w ] .~ = z -> ( -. [ w ] .~ C_ Z <-> -. z e. ~P Z ) )
39 fveq2 
 |-  ( [ w ] .~ = z -> ( # ` [ w ] .~ ) = ( # ` z ) )
40 39 breq2d 
 |-  ( [ w ] .~ = z -> ( P || ( # ` [ w ] .~ ) <-> P || ( # ` z ) ) )
41 38 40 imbi12d 
 |-  ( [ w ] .~ = z -> ( ( -. [ w ] .~ C_ Z -> P || ( # ` [ w ] .~ ) ) <-> ( -. z e. ~P Z -> P || ( # ` z ) ) ) )
42 21 adantr 
 |-  ( ( ph /\ w e. Y ) -> P e. Prime )
43 11 adantr 
 |-  ( ( ph /\ w e. Y ) -> .~ Er Y )
44 simpr 
 |-  ( ( ph /\ w e. Y ) -> w e. Y )
45 43 44 erref 
 |-  ( ( ph /\ w e. Y ) -> w .~ w )
46 vex 
 |-  w e. _V
47 46 46 elec 
 |-  ( w e. [ w ] .~ <-> w .~ w )
48 45 47 sylibr 
 |-  ( ( ph /\ w e. Y ) -> w e. [ w ] .~ )
49 48 ne0d 
 |-  ( ( ph /\ w e. Y ) -> [ w ] .~ =/= (/) )
50 11 ecss 
 |-  ( ph -> [ w ] .~ C_ Y )
51 5 50 ssfid 
 |-  ( ph -> [ w ] .~ e. Fin )
52 51 adantr 
 |-  ( ( ph /\ w e. Y ) -> [ w ] .~ e. Fin )
53 hashnncl 
 |-  ( [ w ] .~ e. Fin -> ( ( # ` [ w ] .~ ) e. NN <-> [ w ] .~ =/= (/) ) )
54 52 53 syl 
 |-  ( ( ph /\ w e. Y ) -> ( ( # ` [ w ] .~ ) e. NN <-> [ w ] .~ =/= (/) ) )
55 49 54 mpbird 
 |-  ( ( ph /\ w e. Y ) -> ( # ` [ w ] .~ ) e. NN )
56 pceq0 
 |-  ( ( P e. Prime /\ ( # ` [ w ] .~ ) e. NN ) -> ( ( P pCnt ( # ` [ w ] .~ ) ) = 0 <-> -. P || ( # ` [ w ] .~ ) ) )
57 42 55 56 syl2anc 
 |-  ( ( ph /\ w e. Y ) -> ( ( P pCnt ( # ` [ w ] .~ ) ) = 0 <-> -. P || ( # ` [ w ] .~ ) ) )
58 oveq2 
 |-  ( ( P pCnt ( # ` [ w ] .~ ) ) = 0 -> ( P ^ ( P pCnt ( # ` [ w ] .~ ) ) ) = ( P ^ 0 ) )
59 hashcl 
 |-  ( [ w ] .~ e. Fin -> ( # ` [ w ] .~ ) e. NN0 )
60 51 59 syl 
 |-  ( ph -> ( # ` [ w ] .~ ) e. NN0 )
61 60 nn0zd 
 |-  ( ph -> ( # ` [ w ] .~ ) e. ZZ )
62 ssrab2 
 |-  { v e. X | ( v .(+) w ) = w } C_ X
63 ssfi 
 |-  ( ( X e. Fin /\ { v e. X | ( v .(+) w ) = w } C_ X ) -> { v e. X | ( v .(+) w ) = w } e. Fin )
64 4 62 63 sylancl 
 |-  ( ph -> { v e. X | ( v .(+) w ) = w } e. Fin )
65 hashcl 
 |-  ( { v e. X | ( v .(+) w ) = w } e. Fin -> ( # ` { v e. X | ( v .(+) w ) = w } ) e. NN0 )
66 64 65 syl 
 |-  ( ph -> ( # ` { v e. X | ( v .(+) w ) = w } ) e. NN0 )
67 66 nn0zd 
 |-  ( ph -> ( # ` { v e. X | ( v .(+) w ) = w } ) e. ZZ )
68 dvdsmul1 
 |-  ( ( ( # ` [ w ] .~ ) e. ZZ /\ ( # ` { v e. X | ( v .(+) w ) = w } ) e. ZZ ) -> ( # ` [ w ] .~ ) || ( ( # ` [ w ] .~ ) x. ( # ` { v e. X | ( v .(+) w ) = w } ) ) )
69 61 67 68 syl2anc 
 |-  ( ph -> ( # ` [ w ] .~ ) || ( ( # ` [ w ] .~ ) x. ( # ` { v e. X | ( v .(+) w ) = w } ) ) )
70 69 adantr 
 |-  ( ( ph /\ w e. Y ) -> ( # ` [ w ] .~ ) || ( ( # ` [ w ] .~ ) x. ( # ` { v e. X | ( v .(+) w ) = w } ) ) )
71 2 adantr 
 |-  ( ( ph /\ w e. Y ) -> .(+) e. ( G GrpAct Y ) )
72 4 adantr 
 |-  ( ( ph /\ w e. Y ) -> X e. Fin )
73 eqid 
 |-  { v e. X | ( v .(+) w ) = w } = { v e. X | ( v .(+) w ) = w }
74 eqid 
 |-  ( G ~QG { v e. X | ( v .(+) w ) = w } ) = ( G ~QG { v e. X | ( v .(+) w ) = w } )
75 1 73 74 7 orbsta2 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ w e. Y ) /\ X e. Fin ) -> ( # ` X ) = ( ( # ` [ w ] .~ ) x. ( # ` { v e. X | ( v .(+) w ) = w } ) ) )
76 71 44 72 75 syl21anc 
 |-  ( ( ph /\ w e. Y ) -> ( # ` X ) = ( ( # ` [ w ] .~ ) x. ( # ` { v e. X | ( v .(+) w ) = w } ) ) )
77 70 76 breqtrrd 
 |-  ( ( ph /\ w e. Y ) -> ( # ` [ w ] .~ ) || ( # ` X ) )
78 20 simprd 
 |-  ( ph -> E. n e. NN0 ( # ` X ) = ( P ^ n ) )
79 78 adantr 
 |-  ( ( ph /\ w e. Y ) -> E. n e. NN0 ( # ` X ) = ( P ^ n ) )
80 breq2 
 |-  ( ( # ` X ) = ( P ^ n ) -> ( ( # ` [ w ] .~ ) || ( # ` X ) <-> ( # ` [ w ] .~ ) || ( P ^ n ) ) )
81 80 biimpcd 
 |-  ( ( # ` [ w ] .~ ) || ( # ` X ) -> ( ( # ` X ) = ( P ^ n ) -> ( # ` [ w ] .~ ) || ( P ^ n ) ) )
82 81 reximdv 
 |-  ( ( # ` [ w ] .~ ) || ( # ` X ) -> ( E. n e. NN0 ( # ` X ) = ( P ^ n ) -> E. n e. NN0 ( # ` [ w ] .~ ) || ( P ^ n ) ) )
83 77 79 82 sylc 
 |-  ( ( ph /\ w e. Y ) -> E. n e. NN0 ( # ` [ w ] .~ ) || ( P ^ n ) )
84 pcprmpw2 
 |-  ( ( P e. Prime /\ ( # ` [ w ] .~ ) e. NN ) -> ( E. n e. NN0 ( # ` [ w ] .~ ) || ( P ^ n ) <-> ( # ` [ w ] .~ ) = ( P ^ ( P pCnt ( # ` [ w ] .~ ) ) ) ) )
85 42 55 84 syl2anc 
 |-  ( ( ph /\ w e. Y ) -> ( E. n e. NN0 ( # ` [ w ] .~ ) || ( P ^ n ) <-> ( # ` [ w ] .~ ) = ( P ^ ( P pCnt ( # ` [ w ] .~ ) ) ) ) )
86 83 85 mpbid 
 |-  ( ( ph /\ w e. Y ) -> ( # ` [ w ] .~ ) = ( P ^ ( P pCnt ( # ` [ w ] .~ ) ) ) )
87 86 eqcomd 
 |-  ( ( ph /\ w e. Y ) -> ( P ^ ( P pCnt ( # ` [ w ] .~ ) ) ) = ( # ` [ w ] .~ ) )
88 23 adantr 
 |-  ( ( ph /\ w e. Y ) -> P e. ZZ )
89 88 zcnd 
 |-  ( ( ph /\ w e. Y ) -> P e. CC )
90 89 exp0d 
 |-  ( ( ph /\ w e. Y ) -> ( P ^ 0 ) = 1 )
91 hash1 
 |-  ( # ` 1o ) = 1
92 90 91 eqtr4di 
 |-  ( ( ph /\ w e. Y ) -> ( P ^ 0 ) = ( # ` 1o ) )
93 87 92 eqeq12d 
 |-  ( ( ph /\ w e. Y ) -> ( ( P ^ ( P pCnt ( # ` [ w ] .~ ) ) ) = ( P ^ 0 ) <-> ( # ` [ w ] .~ ) = ( # ` 1o ) ) )
94 df1o2 
 |-  1o = { (/) }
95 snfi 
 |-  { (/) } e. Fin
96 94 95 eqeltri 
 |-  1o e. Fin
97 hashen 
 |-  ( ( [ w ] .~ e. Fin /\ 1o e. Fin ) -> ( ( # ` [ w ] .~ ) = ( # ` 1o ) <-> [ w ] .~ ~~ 1o ) )
98 52 96 97 sylancl 
 |-  ( ( ph /\ w e. Y ) -> ( ( # ` [ w ] .~ ) = ( # ` 1o ) <-> [ w ] .~ ~~ 1o ) )
99 93 98 bitrd 
 |-  ( ( ph /\ w e. Y ) -> ( ( P ^ ( P pCnt ( # ` [ w ] .~ ) ) ) = ( P ^ 0 ) <-> [ w ] .~ ~~ 1o ) )
100 en1b 
 |-  ( [ w ] .~ ~~ 1o <-> [ w ] .~ = { U. [ w ] .~ } )
101 99 100 bitrdi 
 |-  ( ( ph /\ w e. Y ) -> ( ( P ^ ( P pCnt ( # ` [ w ] .~ ) ) ) = ( P ^ 0 ) <-> [ w ] .~ = { U. [ w ] .~ } ) )
102 44 adantr 
 |-  ( ( ( ph /\ w e. Y ) /\ ( h e. X /\ [ w ] .~ = { U. [ w ] .~ } ) ) -> w e. Y )
103 2 ad2antrr 
 |-  ( ( ( ph /\ w e. Y ) /\ ( h e. X /\ [ w ] .~ = { U. [ w ] .~ } ) ) -> .(+) e. ( G GrpAct Y ) )
104 1 gaf 
 |-  ( .(+) e. ( G GrpAct Y ) -> .(+) : ( X X. Y ) --> Y )
105 103 104 syl 
 |-  ( ( ( ph /\ w e. Y ) /\ ( h e. X /\ [ w ] .~ = { U. [ w ] .~ } ) ) -> .(+) : ( X X. Y ) --> Y )
106 simprl 
 |-  ( ( ( ph /\ w e. Y ) /\ ( h e. X /\ [ w ] .~ = { U. [ w ] .~ } ) ) -> h e. X )
107 105 106 102 fovrnd 
 |-  ( ( ( ph /\ w e. Y ) /\ ( h e. X /\ [ w ] .~ = { U. [ w ] .~ } ) ) -> ( h .(+) w ) e. Y )
108 eqid 
 |-  ( h .(+) w ) = ( h .(+) w )
109 oveq1 
 |-  ( k = h -> ( k .(+) w ) = ( h .(+) w ) )
110 109 eqeq1d 
 |-  ( k = h -> ( ( k .(+) w ) = ( h .(+) w ) <-> ( h .(+) w ) = ( h .(+) w ) ) )
111 110 rspcev 
 |-  ( ( h e. X /\ ( h .(+) w ) = ( h .(+) w ) ) -> E. k e. X ( k .(+) w ) = ( h .(+) w ) )
112 106 108 111 sylancl 
 |-  ( ( ( ph /\ w e. Y ) /\ ( h e. X /\ [ w ] .~ = { U. [ w ] .~ } ) ) -> E. k e. X ( k .(+) w ) = ( h .(+) w ) )
113 7 gaorb 
 |-  ( w .~ ( h .(+) w ) <-> ( w e. Y /\ ( h .(+) w ) e. Y /\ E. k e. X ( k .(+) w ) = ( h .(+) w ) ) )
114 102 107 112 113 syl3anbrc 
 |-  ( ( ( ph /\ w e. Y ) /\ ( h e. X /\ [ w ] .~ = { U. [ w ] .~ } ) ) -> w .~ ( h .(+) w ) )
115 ovex 
 |-  ( h .(+) w ) e. _V
116 115 46 elec 
 |-  ( ( h .(+) w ) e. [ w ] .~ <-> w .~ ( h .(+) w ) )
117 114 116 sylibr 
 |-  ( ( ( ph /\ w e. Y ) /\ ( h e. X /\ [ w ] .~ = { U. [ w ] .~ } ) ) -> ( h .(+) w ) e. [ w ] .~ )
118 simprr 
 |-  ( ( ( ph /\ w e. Y ) /\ ( h e. X /\ [ w ] .~ = { U. [ w ] .~ } ) ) -> [ w ] .~ = { U. [ w ] .~ } )
119 117 118 eleqtrd 
 |-  ( ( ( ph /\ w e. Y ) /\ ( h e. X /\ [ w ] .~ = { U. [ w ] .~ } ) ) -> ( h .(+) w ) e. { U. [ w ] .~ } )
120 115 elsn 
 |-  ( ( h .(+) w ) e. { U. [ w ] .~ } <-> ( h .(+) w ) = U. [ w ] .~ )
121 119 120 sylib 
 |-  ( ( ( ph /\ w e. Y ) /\ ( h e. X /\ [ w ] .~ = { U. [ w ] .~ } ) ) -> ( h .(+) w ) = U. [ w ] .~ )
122 48 adantr 
 |-  ( ( ( ph /\ w e. Y ) /\ ( h e. X /\ [ w ] .~ = { U. [ w ] .~ } ) ) -> w e. [ w ] .~ )
123 122 118 eleqtrd 
 |-  ( ( ( ph /\ w e. Y ) /\ ( h e. X /\ [ w ] .~ = { U. [ w ] .~ } ) ) -> w e. { U. [ w ] .~ } )
124 46 elsn 
 |-  ( w e. { U. [ w ] .~ } <-> w = U. [ w ] .~ )
125 123 124 sylib 
 |-  ( ( ( ph /\ w e. Y ) /\ ( h e. X /\ [ w ] .~ = { U. [ w ] .~ } ) ) -> w = U. [ w ] .~ )
126 121 125 eqtr4d 
 |-  ( ( ( ph /\ w e. Y ) /\ ( h e. X /\ [ w ] .~ = { U. [ w ] .~ } ) ) -> ( h .(+) w ) = w )
127 126 expr 
 |-  ( ( ( ph /\ w e. Y ) /\ h e. X ) -> ( [ w ] .~ = { U. [ w ] .~ } -> ( h .(+) w ) = w ) )
128 127 ralrimdva 
 |-  ( ( ph /\ w e. Y ) -> ( [ w ] .~ = { U. [ w ] .~ } -> A. h e. X ( h .(+) w ) = w ) )
129 101 128 sylbid 
 |-  ( ( ph /\ w e. Y ) -> ( ( P ^ ( P pCnt ( # ` [ w ] .~ ) ) ) = ( P ^ 0 ) -> A. h e. X ( h .(+) w ) = w ) )
130 58 129 syl5 
 |-  ( ( ph /\ w e. Y ) -> ( ( P pCnt ( # ` [ w ] .~ ) ) = 0 -> A. h e. X ( h .(+) w ) = w ) )
131 57 130 sylbird 
 |-  ( ( ph /\ w e. Y ) -> ( -. P || ( # ` [ w ] .~ ) -> A. h e. X ( h .(+) w ) = w ) )
132 oveq2 
 |-  ( u = w -> ( h .(+) u ) = ( h .(+) w ) )
133 id 
 |-  ( u = w -> u = w )
134 132 133 eqeq12d 
 |-  ( u = w -> ( ( h .(+) u ) = u <-> ( h .(+) w ) = w ) )
135 134 ralbidv 
 |-  ( u = w -> ( A. h e. X ( h .(+) u ) = u <-> A. h e. X ( h .(+) w ) = w ) )
136 135 6 elrab2 
 |-  ( w e. Z <-> ( w e. Y /\ A. h e. X ( h .(+) w ) = w ) )
137 136 baib 
 |-  ( w e. Y -> ( w e. Z <-> A. h e. X ( h .(+) w ) = w ) )
138 137 adantl 
 |-  ( ( ph /\ w e. Y ) -> ( w e. Z <-> A. h e. X ( h .(+) w ) = w ) )
139 131 138 sylibrd 
 |-  ( ( ph /\ w e. Y ) -> ( -. P || ( # ` [ w ] .~ ) -> w e. Z ) )
140 1 2 3 4 5 6 7 sylow2alem1 
 |-  ( ( ph /\ w e. Z ) -> [ w ] .~ = { w } )
141 simpr 
 |-  ( ( ph /\ w e. Z ) -> w e. Z )
142 141 snssd 
 |-  ( ( ph /\ w e. Z ) -> { w } C_ Z )
143 140 142 eqsstrd 
 |-  ( ( ph /\ w e. Z ) -> [ w ] .~ C_ Z )
144 143 ex 
 |-  ( ph -> ( w e. Z -> [ w ] .~ C_ Z ) )
145 144 adantr 
 |-  ( ( ph /\ w e. Y ) -> ( w e. Z -> [ w ] .~ C_ Z ) )
146 139 145 syld 
 |-  ( ( ph /\ w e. Y ) -> ( -. P || ( # ` [ w ] .~ ) -> [ w ] .~ C_ Z ) )
147 146 con1d 
 |-  ( ( ph /\ w e. Y ) -> ( -. [ w ] .~ C_ Z -> P || ( # ` [ w ] .~ ) ) )
148 34 41 147 ectocld 
 |-  ( ( ph /\ z e. ( Y /. .~ ) ) -> ( -. z e. ~P Z -> P || ( # ` z ) ) )
149 148 impr 
 |-  ( ( ph /\ ( z e. ( Y /. .~ ) /\ -. z e. ~P Z ) ) -> P || ( # ` z ) )
150 33 149 sylan2b 
 |-  ( ( ph /\ z e. ( ( Y /. .~ ) \ ~P Z ) ) -> P || ( # ` z ) )
151 15 23 32 150 fsumdvds 
 |-  ( ph -> P || sum_ z e. ( ( Y /. .~ ) \ ~P Z ) ( # ` z ) )