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 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 ∈ 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