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 = Base G
sylow1.g ⊢ φ → G ∈ Grp
sylow1.f ⊢ φ → X ∈ Fin
sylow1.p ⊢ φ → P ∈ ℙ
sylow1.n ⊢ φ → N ∈ ℕ 0
sylow1.d ⊢ φ → P N ∥ X
sylow1lem.a ⊢ + ˙ = + G
sylow1lem.s ⊢ S = s ∈ 𝒫 X | s = P N
sylow1lem.m ⊢ ⊕ ˙ = x ∈ X , y ∈ S ⟼ ran ⁡ z ∈ y ⟼ x + ˙ z
sylow1lem3.1 ⊢ ∼ ˙ = x y | x y ⊆ S ∧ ∃ g ∈ X g ⊕ ˙ x = y
Assertion sylow1lem3 ⊢ φ → ∃ w ∈ S P pCnt w ∼ ˙ ≤ P pCnt X − N

Proof

Step Hyp Ref Expression
1 sylow1.x ⊢ X = Base G
2 sylow1.g ⊢ φ → G ∈ Grp
3 sylow1.f ⊢ φ → X ∈ Fin
4 sylow1.p ⊢ φ → P ∈ ℙ
5 sylow1.n ⊢ φ → N ∈ ℕ 0
6 sylow1.d ⊢ φ → P N ∥ X
7 sylow1lem.a ⊢ + ˙ = + G
8 sylow1lem.s ⊢ S = s ∈ 𝒫 X | s = P N
9 sylow1lem.m ⊢ ⊕ ˙ = x ∈ X , y ∈ S ⟼ ran ⁡ z ∈ y ⟼ x + ˙ z
10 sylow1lem3.1 ⊢ ∼ ˙ = x y | x y ⊆ S ∧ ∃ g ∈ X g ⊕ ˙ x = y
11 1 2 3 4 5 6 7 8 sylow1lem1 ⊢ φ → S ∈ ℕ ∧ P pCnt S = P pCnt X − N
12 11 simpld ⊢ φ → S ∈ ℕ
13 pcndvds ⊢ P ∈ ℙ ∧ S ∈ ℕ → ¬ P P pCnt S + 1 ∥ S
14 4 12 13 syl2anc ⊢ φ → ¬ P P pCnt S + 1 ∥ S
15 11 simprd ⊢ φ → P pCnt S = P pCnt X − N
16 15 oveq1d ⊢ φ → P pCnt S + 1 = P pCnt X - N + 1
17 16 oveq2d ⊢ φ → P P pCnt S + 1 = P P pCnt X - N + 1
18 1 2 3 4 5 6 7 8 9 sylow1lem2 ⊢ φ → ⊕ ˙ ∈ G GrpAct S
19 10 1 gaorber ⊢ ⊕ ˙ ∈ G GrpAct S → ∼ ˙ Er S
20 18 19 syl ⊢ φ → ∼ ˙ Er S
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 ⊢ φ → P P pCnt S + 1 ∥ S ↔ P P pCnt X - N + 1 ∥ ∑ z ∈ S / ∼ ˙ z
28 14 27 mtbid ⊢ φ → ¬ P P pCnt X - 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 / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N → S / ∼ ˙ ∈ Fin
34 prmnn ⊢ P ∈ ℙ → P ∈ ℕ
35 4 34 syl ⊢ φ → P ∈ ℕ
36 4 12 pccld ⊢ φ → P pCnt S ∈ ℕ 0
37 15 36 eqeltrrd ⊢ φ → P pCnt X − N ∈ ℕ 0
38 peano2nn0 ⊢ P pCnt X − N ∈ ℕ 0 → P pCnt X - N + 1 ∈ ℕ 0
39 37 38 syl ⊢ φ → P pCnt X - N + 1 ∈ ℕ 0
40 35 39 nnexpcld ⊢ φ → P P pCnt X - N + 1 ∈ ℕ
41 40 nnzd ⊢ φ → P P pCnt X - N + 1 ∈ ℤ
42 41 adantr ⊢ φ ∧ ∀ a ∈ S / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N → P P pCnt X - N + 1 ∈ ℤ
43 erdm ⊢ ∼ ˙ Er S → 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 / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N ∧ z ∈ S / ∼ ˙ → z ∈ ℕ
55 54 nnzd ⊢ φ ∧ ∀ a ∈ S / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N ∧ z ∈ S / ∼ ˙ → z ∈ ℤ
56 fveq2 ⊢ a = z → a = z
57 56 oveq2d ⊢ a = z → P pCnt a = P pCnt z
58 57 breq1d ⊢ a = z → P pCnt a ≤ P pCnt X − N ↔ P pCnt z ≤ P pCnt X − N
59 58 notbid ⊢ a = z → ¬ P pCnt a ≤ P pCnt X − N ↔ ¬ P pCnt z ≤ P pCnt X − N
60 59 rspccva ⊢ ∀ a ∈ S / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N ∧ z ∈ S / ∼ ˙ → ¬ P pCnt z ≤ P pCnt X − N
61 60 adantll ⊢ φ ∧ ∀ a ∈ S / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N ∧ z ∈ S / ∼ ˙ → ¬ P pCnt z ≤ P pCnt X − 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 ⊢ φ → P pCnt X ∈ ℕ 0
68 67 nn0zd ⊢ φ → P pCnt X ∈ ℤ
69 5 nn0zd ⊢ φ → N ∈ ℤ
70 68 69 zsubcld ⊢ φ → P pCnt X − N ∈ ℤ
71 70 ad2antrr ⊢ φ ∧ ∀ a ∈ S / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N ∧ z ∈ S / ∼ ˙ → P pCnt X − N ∈ ℤ
72 71 zred ⊢ φ ∧ ∀ a ∈ S / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N ∧ z ∈ S / ∼ ˙ → P pCnt X − N ∈ ℝ
73 4 ad2antrr ⊢ φ ∧ ∀ a ∈ S / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N ∧ z ∈ S / ∼ ˙ → P ∈ ℙ
74 73 54 pccld ⊢ φ ∧ ∀ a ∈ S / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N ∧ z ∈ S / ∼ ˙ → P pCnt z ∈ ℕ 0
75 74 nn0zd ⊢ φ ∧ ∀ a ∈ S / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N ∧ z ∈ S / ∼ ˙ → P pCnt z ∈ ℤ
76 75 zred ⊢ φ ∧ ∀ a ∈ S / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N ∧ z ∈ S / ∼ ˙ → P pCnt z ∈ ℝ
77 72 76 ltnled ⊢ φ ∧ ∀ a ∈ S / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N ∧ z ∈ S / ∼ ˙ → P pCnt X − N < P pCnt z ↔ ¬ P pCnt z ≤ P pCnt X − N
78 61 77 mpbird ⊢ φ ∧ ∀ a ∈ S / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N ∧ z ∈ S / ∼ ˙ → P pCnt X − N < P pCnt z
79 zltp1le ⊢ P pCnt X − N ∈ ℤ ∧ P pCnt z ∈ ℤ → P pCnt X − N < P pCnt z ↔ P pCnt X - N + 1 ≤ P pCnt z
80 71 75 79 syl2anc ⊢ φ ∧ ∀ a ∈ S / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N ∧ z ∈ S / ∼ ˙ → P pCnt X − N < P pCnt z ↔ P pCnt X - N + 1 ≤ P pCnt z
81 78 80 mpbid ⊢ φ ∧ ∀ a ∈ S / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N ∧ z ∈ S / ∼ ˙ → P pCnt X - N + 1 ≤ P pCnt z
82 39 ad2antrr ⊢ φ ∧ ∀ a ∈ S / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N ∧ z ∈ S / ∼ ˙ → P pCnt X - N + 1 ∈ ℕ 0
83 pcdvdsb ⊢ P ∈ ℙ ∧ z ∈ ℤ ∧ P pCnt X - N + 1 ∈ ℕ 0 → P pCnt X - N + 1 ≤ P pCnt z ↔ P P pCnt X - N + 1 ∥ z
84 73 55 82 83 syl3anc ⊢ φ ∧ ∀ a ∈ S / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N ∧ z ∈ S / ∼ ˙ → P pCnt X - N + 1 ≤ P pCnt z ↔ P P pCnt X - N + 1 ∥ z
85 81 84 mpbid ⊢ φ ∧ ∀ a ∈ S / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N ∧ z ∈ S / ∼ ˙ → P P pCnt X - N + 1 ∥ z
86 33 42 55 85 fsumdvds ⊢ φ ∧ ∀ a ∈ S / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N → P P pCnt X - N + 1 ∥ ∑ z ∈ S / ∼ ˙ z
87 28 86 mtand ⊢ φ → ¬ ∀ a ∈ S / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N
88 dfrex2 ⊢ ∃ a ∈ S / ∼ ˙ P pCnt a ≤ P pCnt X − N ↔ ¬ ∀ a ∈ S / ∼ ˙ ¬ P pCnt a ≤ P pCnt X − N
89 87 88 sylibr ⊢ φ → ∃ a ∈ S / ∼ ˙ P pCnt a ≤ P pCnt X − N
90 eqid ⊢ S / ∼ ˙ = S / ∼ ˙
91 fveq2 ⊢ z ∼ ˙ = a → z ∼ ˙ = a
92 91 oveq2d ⊢ z ∼ ˙ = a → P pCnt z ∼ ˙ = P pCnt a
93 92 breq1d ⊢ z ∼ ˙ = a → P pCnt z ∼ ˙ ≤ P pCnt X − N ↔ P pCnt a ≤ P pCnt X − N
94 93 imbi1d ⊢ z ∼ ˙ = a → P pCnt z ∼ ˙ ≤ P pCnt X − N → ∃ w ∈ S P pCnt w ∼ ˙ ≤ P pCnt X − N ↔ P pCnt a ≤ P pCnt X − N → ∃ w ∈ S P pCnt w ∼ ˙ ≤ P pCnt X − N
95 eceq1 ⊢ w = z → w ∼ ˙ = z ∼ ˙
96 95 fveq2d ⊢ w = z → w ∼ ˙ = z ∼ ˙
97 96 oveq2d ⊢ w = z → P pCnt w ∼ ˙ = P pCnt z ∼ ˙
98 97 breq1d ⊢ w = z → P pCnt w ∼ ˙ ≤ P pCnt X − N ↔ P pCnt z ∼ ˙ ≤ P pCnt X − N
99 98 rspcev ⊢ z ∈ S ∧ P pCnt z ∼ ˙ ≤ P pCnt X − N → ∃ w ∈ S P pCnt w ∼ ˙ ≤ P pCnt X − N
100 99 ex ⊢ z ∈ S → P pCnt z ∼ ˙ ≤ P pCnt X − N → ∃ w ∈ S P pCnt w ∼ ˙ ≤ P pCnt X − N
101 100 adantl ⊢ φ ∧ z ∈ S → P pCnt z ∼ ˙ ≤ P pCnt X − N → ∃ w ∈ S P pCnt w ∼ ˙ ≤ P pCnt X − N
102 90 94 101 ectocld ⊢ φ ∧ a ∈ S / ∼ ˙ → P pCnt a ≤ P pCnt X − N → ∃ w ∈ S P pCnt w ∼ ˙ ≤ P pCnt X − N
103 102 rexlimdva ⊢ φ → ∃ a ∈ S / ∼ ˙ P pCnt a ≤ P pCnt X − N → ∃ w ∈ S P pCnt w ∼ ˙ ≤ P pCnt X − N
104 89 103 mpd ⊢ φ → ∃ w ∈ S P pCnt w ∼ ˙ ≤ P pCnt X − N