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=BaseG
sylow2a.m ⊢φ→⊕˙∈GGrpActY
sylow2a.p ⊢φ→PpGrpG
sylow2a.f ⊢φ→X∈Fin
sylow2a.y ⊢φ→Y∈Fin
sylow2a.z ⊢Z=u∈Y|∀h∈Xh⊕˙u=u
sylow2a.r ⊢∼˙=xy|xy⊆Y∧∃g∈Xg⊕˙x=y
Assertion sylow2alem2 ⊢φ→P∥∑z∈Y/∼˙∖𝒫Zz

Proof

Step Hyp Ref Expression
1 sylow2a.x ⊢X=BaseG
2 sylow2a.m ⊢φ→⊕˙∈GGrpActY
3 sylow2a.p ⊢φ→PpGrpG
4 sylow2a.f ⊢φ→X∈Fin
5 sylow2a.y ⊢φ→Y∈Fin
6 sylow2a.z ⊢Z=u∈Y|∀h∈Xh⊕˙u=u
7 sylow2a.r ⊢∼˙=xy|xy⊆Y∧∃g∈Xg⊕˙x=y
8 pwfi ⊢Y∈Fin↔𝒫Y∈Fin
9 5 8 sylib ⊢φ→𝒫Y∈Fin
10 7 1 gaorber ⊢⊕˙∈GGrpActY→∼˙ErY
11 2 10 syl ⊢φ→∼˙ErY
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 ⊢⊕˙∈GGrpActY→G∈Grp
17 2 16 syl ⊢φ→G∈Grp
18 1 pgpfi ⊢G∈Grp∧X∈Fin→PpGrpG↔P∈ℙ∧∃n∈ℕ0X=Pn
19 17 4 18 syl2anc ⊢φ→PpGrpG↔P∈ℙ∧∃n∈ℕ0X=Pn
20 3 19 mpbid ⊢φ→P∈ℙ∧∃n∈ℕ0X=Pn
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→∼˙ErY
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∼˙∈ℕ→PpCntw∼˙=0↔¬P∥w∼˙
57 42 55 56 syl2anc ⊢φ∧w∈Y→PpCntw∼˙=0↔¬P∥w∼˙
58 oveq2 ⊢PpCntw∼˙=0→PPpCntw∼˙=P0
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→⊕˙∈GGrpActY
72 4 adantr ⊢φ∧w∈Y→X∈Fin
73 eqid ⊢v∈X|v⊕˙w=w=v∈X|v⊕˙w=w
74 eqid ⊢G~QGv∈X|v⊕˙w=w=G~QGv∈X|v⊕˙w=w
75 1 73 74 7 orbsta2 ⊢⊕˙∈GGrpActY∧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∈ℕ0X=Pn
79 78 adantr ⊢φ∧w∈Y→∃n∈ℕ0X=Pn
80 breq2 ⊢X=Pn→w∼˙∥X↔w∼˙∥Pn
81 80 biimpcd ⊢w∼˙∥X→X=Pn→w∼˙∥Pn
82 81 reximdv ⊢w∼˙∥X→∃n∈ℕ0X=Pn→∃n∈ℕ0w∼˙∥Pn
83 77 79 82 sylc ⊢φ∧w∈Y→∃n∈ℕ0w∼˙∥Pn
84 pcprmpw2 ⊢P∈ℙ∧w∼˙∈ℕ→∃n∈ℕ0w∼˙∥Pn↔w∼˙=PPpCntw∼˙
85 42 55 84 syl2anc ⊢φ∧w∈Y→∃n∈ℕ0w∼˙∥Pn↔w∼˙=PPpCntw∼˙
86 83 85 mpbid ⊢φ∧w∈Y→w∼˙=PPpCntw∼˙
87 86 eqcomd ⊢φ∧w∈Y→PPpCntw∼˙=w∼˙
88 23 adantr ⊢φ∧w∈Y→P∈ℤ
89 88 zcnd ⊢φ∧w∈Y→P∈ℂ
90 89 exp0d ⊢φ∧w∈Y→P0=1
91 hash1 ⊢1𝑜=1
92 90 91 eqtr4di ⊢φ∧w∈Y→P0=1𝑜
93 87 92 eqeq12d ⊢φ∧w∈Y→PPpCntw∼˙=P0↔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→PPpCntw∼˙=P0↔w∼˙≈1𝑜
100 en1b ⊢w∼˙≈1𝑜↔w∼˙=⋃w∼˙
101 99 100 bitrdi ⊢φ∧w∈Y→PPpCntw∼˙=P0↔w∼˙=⋃w∼˙
102 44 adantr ⊢φ∧w∈Y∧h∈X∧w∼˙=⋃w∼˙→w∈Y
103 2 ad2antrr ⊢φ∧w∈Y∧h∈X∧w∼˙=⋃w∼˙→⊕˙∈GGrpActY
104 1 gaf ⊢⊕˙∈GGrpActY→⊕˙: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 fovcdmd ⊢φ∧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∈Xk⊕˙w=h⊕˙w
112 106 108 111 sylancl ⊢φ∧w∈Y∧h∈X∧w∼˙=⋃w∼˙→∃k∈Xk⊕˙w=h⊕˙w
113 7 gaorb ⊢w∼˙h⊕˙w↔w∈Y∧h⊕˙w∈Y∧∃k∈Xk⊕˙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∈Xh⊕˙w=w
129 101 128 sylbid ⊢φ∧w∈Y→PPpCntw∼˙=P0→∀h∈Xh⊕˙w=w
130 58 129 syl5 ⊢φ∧w∈Y→PpCntw∼˙=0→∀h∈Xh⊕˙w=w
131 57 130 sylbird ⊢φ∧w∈Y→¬P∥w∼˙→∀h∈Xh⊕˙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∈Xh⊕˙u=u↔∀h∈Xh⊕˙w=w
136 135 6 elrab2 ⊢w∈Z↔w∈Y∧∀h∈Xh⊕˙w=w
137 136 baib ⊢w∈Y→w∈Z↔∀h∈Xh⊕˙w=w
138 137 adantl ⊢φ∧w∈Y→w∈Z↔∀h∈Xh⊕˙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/∼˙∖𝒫Zz