Metamath Proof Explorer

Theorem sylow1lem3

Description: Lemma for sylow1 . One of the orbits of the group action has p-adic valuation less than the prime count of the set S . (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Hypotheses sylow1.x ⊢X=BaseG
sylow1.g ⊢φ→G∈Grp
sylow1.f ⊢φ→X∈Fin
sylow1.p ⊢φ→P∈ℙ
sylow1.n ⊢φ→N∈ℕ0
sylow1.d ⊢φ→PN∥X
sylow1lem.a ⊢+˙=+G
sylow1lem.s ⊢S=s∈𝒫X|s=PN
sylow1lem.m ⊢⊕˙=x∈X,y∈S⟼ran⁡z∈y⟼x+˙z
sylow1lem3.1 ⊢∼˙=xy|xy⊆S∧∃g∈Xg⊕˙x=y
Assertion sylow1lem3 ⊢φ→∃w∈SPpCntw∼˙≤PpCntX−N

Proof

Step Hyp Ref Expression
1 sylow1.x ⊢X=BaseG
2 sylow1.g ⊢φ→G∈Grp
3 sylow1.f ⊢φ→X∈Fin
4 sylow1.p ⊢φ→P∈ℙ
5 sylow1.n ⊢φ→N∈ℕ0
6 sylow1.d ⊢φ→PN∥X
7 sylow1lem.a ⊢+˙=+G
8 sylow1lem.s ⊢S=s∈𝒫X|s=PN
9 sylow1lem.m ⊢⊕˙=x∈X,y∈S⟼ran⁡z∈y⟼x+˙z
10 sylow1lem3.1 ⊢∼˙=xy|xy⊆S∧∃g∈Xg⊕˙x=y
11 1 2 3 4 5 6 7 8 sylow1lem1 ⊢φ→S∈ℕ∧PpCntS=PpCntX−N
12 11 simpld ⊢φ→S∈ℕ
13 pcndvds ⊢P∈ℙ∧S∈ℕ→¬PPpCntS+1∥S
14 4 12 13 syl2anc ⊢φ→¬PPpCntS+1∥S
15 11 simprd ⊢φ→PpCntS=PpCntX−N
16 15 oveq1d ⊢φ→PpCntS+1=PpCntX-N+1
17 16 oveq2d ⊢φ→PPpCntS+1=PPpCntX-N+1
18 1 2 3 4 5 6 7 8 9 sylow1lem2 ⊢φ→⊕˙∈GGrpActS
19 10 1 gaorber ⊢⊕˙∈GGrpActS→∼˙ErS
20 18 19 syl ⊢φ→∼˙ErS
21 pwfi ⊢X∈Fin↔𝒫X∈Fin
22 3 21 sylib ⊢φ→𝒫X∈Fin
23 8 ssrab3 ⊢S⊆𝒫X
24 ssfi ⊢𝒫X∈Fin∧S⊆𝒫X→S∈Fin
25 22 23 24 sylancl ⊢φ→S∈Fin
26 20 25 qshash ⊢φ→S=∑z∈S/∼˙z
27 17 26 breq12d ⊢φ→PPpCntS+1∥S↔PPpCntX-N+1∥∑z∈S/∼˙z
28 14 27 mtbid ⊢φ→¬PPpCntX-N+1∥∑z∈S/∼˙z
29 pwfi ⊢S∈Fin↔𝒫S∈Fin
30 25 29 sylib ⊢φ→𝒫S∈Fin
31 20 qsss ⊢φ→S/∼˙⊆𝒫S
32 30 31 ssfid ⊢φ→S/∼˙∈Fin
33 32 adantr ⊢φ∧∀a∈S/∼˙¬PpCnta≤PpCntX−N→S/∼˙∈Fin
34 prmnn ⊢P∈ℙ→P∈ℕ
35 4 34 syl ⊢φ→P∈ℕ
36 4 12 pccld ⊢φ→PpCntS∈ℕ0
37 15 36 eqeltrrd ⊢φ→PpCntX−N∈ℕ0
38 peano2nn0 ⊢PpCntX−N∈ℕ0→PpCntX-N+1∈ℕ0
39 37 38 syl ⊢φ→PpCntX-N+1∈ℕ0
40 35 39 nnexpcld ⊢φ→PPpCntX-N+1∈ℕ
41 40 nnzd ⊢φ→PPpCntX-N+1∈ℤ
42 41 adantr ⊢φ∧∀a∈S/∼˙¬PpCnta≤PpCntX−N→PPpCntX-N+1∈ℤ
43 erdm ⊢∼˙ErS→dom⁡∼˙=S
44 20 43 syl ⊢φ→dom⁡∼˙=S
45 elqsn0 ⊢dom⁡∼˙=S∧z∈S/∼˙→z≠∅
46 44 45 sylan ⊢φ∧z∈S/∼˙→z≠∅
47 25 adantr ⊢φ∧z∈S/∼˙→S∈Fin
48 31 sselda ⊢φ∧z∈S/∼˙→z∈𝒫S
49 48 elpwid ⊢φ∧z∈S/∼˙→z⊆S
50 47 49 ssfid ⊢φ∧z∈S/∼˙→z∈Fin
51 hashnncl ⊢z∈Fin→z∈ℕ↔z≠∅
52 50 51 syl ⊢φ∧z∈S/∼˙→z∈ℕ↔z≠∅
53 46 52 mpbird ⊢φ∧z∈S/∼˙→z∈ℕ
54 53 adantlr ⊢φ∧∀a∈S/∼˙¬PpCnta≤PpCntX−N∧z∈S/∼˙→z∈ℕ
55 54 nnzd ⊢φ∧∀a∈S/∼˙¬PpCnta≤PpCntX−N∧z∈S/∼˙→z∈ℤ
56 fveq2 ⊢a=z→a=z
57 56 oveq2d ⊢a=z→PpCnta=PpCntz
58 57 breq1d ⊢a=z→PpCnta≤PpCntX−N↔PpCntz≤PpCntX−N
59 58 notbid ⊢a=z→¬PpCnta≤PpCntX−N↔¬PpCntz≤PpCntX−N
60 59 rspccva ⊢∀a∈S/∼˙¬PpCnta≤PpCntX−N∧z∈S/∼˙→¬PpCntz≤PpCntX−N
61 60 adantll ⊢φ∧∀a∈S/∼˙¬PpCnta≤PpCntX−N∧z∈S/∼˙→¬PpCntz≤PpCntX−N
62 1 grpbn0 ⊢G∈Grp→X≠∅
63 2 62 syl ⊢φ→X≠∅
64 hashnncl ⊢X∈Fin→X∈ℕ↔X≠∅
65 3 64 syl ⊢φ→X∈ℕ↔X≠∅
66 63 65 mpbird ⊢φ→X∈ℕ
67 4 66 pccld ⊢φ→PpCntX∈ℕ0
68 67 nn0zd ⊢φ→PpCntX∈ℤ
69 5 nn0zd ⊢φ→N∈ℤ
70 68 69 zsubcld ⊢φ→PpCntX−N∈ℤ
71 70 ad2antrr ⊢φ∧∀a∈S/∼˙¬PpCnta≤PpCntX−N∧z∈S/∼˙→PpCntX−N∈ℤ
72 71 zred ⊢φ∧∀a∈S/∼˙¬PpCnta≤PpCntX−N∧z∈S/∼˙→PpCntX−N∈ℝ
73 4 ad2antrr ⊢φ∧∀a∈S/∼˙¬PpCnta≤PpCntX−N∧z∈S/∼˙→P∈ℙ
74 73 54 pccld ⊢φ∧∀a∈S/∼˙¬PpCnta≤PpCntX−N∧z∈S/∼˙→PpCntz∈ℕ0
75 74 nn0zd ⊢φ∧∀a∈S/∼˙¬PpCnta≤PpCntX−N∧z∈S/∼˙→PpCntz∈ℤ
76 75 zred ⊢φ∧∀a∈S/∼˙¬PpCnta≤PpCntX−N∧z∈S/∼˙→PpCntz∈ℝ
77 72 76 ltnled ⊢φ∧∀a∈S/∼˙¬PpCnta≤PpCntX−N∧z∈S/∼˙→PpCntX−N<PpCntz↔¬PpCntz≤PpCntX−N
78 61 77 mpbird ⊢φ∧∀a∈S/∼˙¬PpCnta≤PpCntX−N∧z∈S/∼˙→PpCntX−N<PpCntz
79 zltp1le ⊢PpCntX−N∈ℤ∧PpCntz∈ℤ→PpCntX−N<PpCntz↔PpCntX-N+1≤PpCntz
80 71 75 79 syl2anc ⊢φ∧∀a∈S/∼˙¬PpCnta≤PpCntX−N∧z∈S/∼˙→PpCntX−N<PpCntz↔PpCntX-N+1≤PpCntz
81 78 80 mpbid ⊢φ∧∀a∈S/∼˙¬PpCnta≤PpCntX−N∧z∈S/∼˙→PpCntX-N+1≤PpCntz
82 39 ad2antrr ⊢φ∧∀a∈S/∼˙¬PpCnta≤PpCntX−N∧z∈S/∼˙→PpCntX-N+1∈ℕ0
83 pcdvdsb ⊢P∈ℙ∧z∈ℤ∧PpCntX-N+1∈ℕ0→PpCntX-N+1≤PpCntz↔PPpCntX-N+1∥z
84 73 55 82 83 syl3anc ⊢φ∧∀a∈S/∼˙¬PpCnta≤PpCntX−N∧z∈S/∼˙→PpCntX-N+1≤PpCntz↔PPpCntX-N+1∥z
85 81 84 mpbid ⊢φ∧∀a∈S/∼˙¬PpCnta≤PpCntX−N∧z∈S/∼˙→PPpCntX-N+1∥z
86 33 42 55 85 fsumdvds ⊢φ∧∀a∈S/∼˙¬PpCnta≤PpCntX−N→PPpCntX-N+1∥∑z∈S/∼˙z
87 28 86 mtand ⊢φ→¬∀a∈S/∼˙¬PpCnta≤PpCntX−N
88 dfrex2 ⊢∃a∈S/∼˙PpCnta≤PpCntX−N↔¬∀a∈S/∼˙¬PpCnta≤PpCntX−N
89 87 88 sylibr ⊢φ→∃a∈S/∼˙PpCnta≤PpCntX−N
90 eqid ⊢S/∼˙=S/∼˙
91 fveq2 ⊢z∼˙=a→z∼˙=a
92 91 oveq2d ⊢z∼˙=a→PpCntz∼˙=PpCnta
93 92 breq1d ⊢z∼˙=a→PpCntz∼˙≤PpCntX−N↔PpCnta≤PpCntX−N
94 93 imbi1d ⊢z∼˙=a→PpCntz∼˙≤PpCntX−N→∃w∈SPpCntw∼˙≤PpCntX−N↔PpCnta≤PpCntX−N→∃w∈SPpCntw∼˙≤PpCntX−N
95 eceq1 ⊢w=z→w∼˙=z∼˙
96 95 fveq2d ⊢w=z→w∼˙=z∼˙
97 96 oveq2d ⊢w=z→PpCntw∼˙=PpCntz∼˙
98 97 breq1d ⊢w=z→PpCntw∼˙≤PpCntX−N↔PpCntz∼˙≤PpCntX−N
99 98 rspcev ⊢z∈S∧PpCntz∼˙≤PpCntX−N→∃w∈SPpCntw∼˙≤PpCntX−N
100 99 ex ⊢z∈S→PpCntz∼˙≤PpCntX−N→∃w∈SPpCntw∼˙≤PpCntX−N
101 100 adantl ⊢φ∧z∈S→PpCntz∼˙≤PpCntX−N→∃w∈SPpCntw∼˙≤PpCntX−N
102 90 94 101 ectocld ⊢φ∧a∈S/∼˙→PpCnta≤PpCntX−N→∃w∈SPpCntw∼˙≤PpCntX−N
103 102 rexlimdva ⊢φ→∃a∈S/∼˙PpCnta≤PpCntX−N→∃w∈SPpCntw∼˙≤PpCntX−N
104 89 103 mpd ⊢φ→∃w∈SPpCntw∼˙≤PpCntX−N