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 φ ˙ G GrpAct Y
sylow2a.p φ P pGrp G
sylow2a.f φ X Fin
sylow2a.y φ Y Fin
sylow2a.z Z = u Y | h X h ˙ u = u
sylow2a.r ˙ = x y | x y Y g X g ˙ x = y
Assertion sylow2alem2 φ P z Y / ˙ 𝒫 Z z

Proof

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