Metamath Proof Explorer

Theorem sylow1lem5

Description: Lemma for sylow1 . Using Lagrange's theorem and the orbit-stabilizer theorem, show that there is a subgroup with size exactly P ^ N . (Contributed by Mario Carneiro, 16-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
sylow1lem4.b ⊢ φ → B ∈ S
sylow1lem4.h ⊢ H = u ∈ X | u ⊕ ˙ B = B
sylow1lem5.l ⊢ φ → P pCnt B ∼ ˙ ≤ P pCnt X − N
Assertion sylow1lem5 ⊢ φ → ∃ h ∈ SubGrp ⁡ G h = P 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 sylow1lem4.b ⊢ φ → B ∈ S
12 sylow1lem4.h ⊢ H = u ∈ X | u ⊕ ˙ B = B
13 sylow1lem5.l ⊢ φ → P pCnt B ∼ ˙ ≤ P pCnt X − N
14 1 2 3 4 5 6 7 8 9 sylow1lem2 ⊢ φ → ⊕ ˙ ∈ G GrpAct S
15 1 12 gastacl ⊢ ⊕ ˙ ∈ G GrpAct S ∧ B ∈ S → H ∈ SubGrp ⁡ G
16 14 11 15 syl2anc ⊢ φ → H ∈ SubGrp ⁡ G
17 1 2 3 4 5 6 7 8 9 10 11 12 sylow1lem4 ⊢ φ → H ≤ P N
18 10 1 gaorber ⊢ ⊕ ˙ ∈ G GrpAct S → ∼ ˙ Er S
19 14 18 syl ⊢ φ → ∼ ˙ Er S
20 erdm ⊢ ∼ ˙ Er S → dom ⁡ ∼ ˙ = S
21 19 20 syl ⊢ φ → dom ⁡ ∼ ˙ = S
22 11 21 eleqtrrd ⊢ φ → B ∈ dom ⁡ ∼ ˙
23 ecdmn0 ⊢ B ∈ dom ⁡ ∼ ˙ ↔ B ∼ ˙ ≠ ∅
24 22 23 sylib ⊢ φ → B ∼ ˙ ≠ ∅
25 pwfi ⊢ X ∈ Fin ↔ 𝒫 X ∈ Fin
26 3 25 sylib ⊢ φ → 𝒫 X ∈ Fin
27 8 ssrab3 ⊢ S ⊆ 𝒫 X
28 ssfi ⊢ 𝒫 X ∈ Fin ∧ S ⊆ 𝒫 X → S ∈ Fin
29 26 27 28 sylancl ⊢ φ → S ∈ Fin
30 19 ecss ⊢ φ → B ∼ ˙ ⊆ S
31 29 30 ssfid ⊢ φ → B ∼ ˙ ∈ Fin
32 hashnncl ⊢ B ∼ ˙ ∈ Fin → B ∼ ˙ ∈ ℕ ↔ B ∼ ˙ ≠ ∅
33 31 32 syl ⊢ φ → B ∼ ˙ ∈ ℕ ↔ B ∼ ˙ ≠ ∅
34 24 33 mpbird ⊢ φ → B ∼ ˙ ∈ ℕ
35 4 34 pccld ⊢ φ → P pCnt B ∼ ˙ ∈ ℕ 0
36 35 nn0red ⊢ φ → P pCnt B ∼ ˙ ∈ ℝ
37 5 nn0red ⊢ φ → N ∈ ℝ
38 1 grpbn0 ⊢ G ∈ Grp → X ≠ ∅
39 2 38 syl ⊢ φ → X ≠ ∅
40 hashnncl ⊢ X ∈ Fin → X ∈ ℕ ↔ X ≠ ∅
41 3 40 syl ⊢ φ → X ∈ ℕ ↔ X ≠ ∅
42 39 41 mpbird ⊢ φ → X ∈ ℕ
43 4 42 pccld ⊢ φ → P pCnt X ∈ ℕ 0
44 43 nn0red ⊢ φ → P pCnt X ∈ ℝ
45 leaddsub ⊢ P pCnt B ∼ ˙ ∈ ℝ ∧ N ∈ ℝ ∧ P pCnt X ∈ ℝ → P pCnt B ∼ ˙ + N ≤ P pCnt X ↔ P pCnt B ∼ ˙ ≤ P pCnt X − N
46 36 37 44 45 syl3anc ⊢ φ → P pCnt B ∼ ˙ + N ≤ P pCnt X ↔ P pCnt B ∼ ˙ ≤ P pCnt X − N
47 13 46 mpbird ⊢ φ → P pCnt B ∼ ˙ + N ≤ P pCnt X
48 eqid ⊢ G ~ QG H = G ~ QG H
49 1 12 48 10 orbsta2 ⊢ ⊕ ˙ ∈ G GrpAct S ∧ B ∈ S ∧ X ∈ Fin → X = B ∼ ˙ ⁢ H
50 14 11 3 49 syl21anc ⊢ φ → X = B ∼ ˙ ⁢ H
51 50 oveq2d ⊢ φ → P pCnt X = P pCnt B ∼ ˙ ⁢ H
52 34 nnzd ⊢ φ → B ∼ ˙ ∈ ℤ
53 34 nnne0d ⊢ φ → B ∼ ˙ ≠ 0
54 eqid ⊢ 0 G = 0 G
55 54 subg0cl ⊢ H ∈ SubGrp ⁡ G → 0 G ∈ H
56 16 55 syl ⊢ φ → 0 G ∈ H
57 56 ne0d ⊢ φ → H ≠ ∅
58 12 ssrab3 ⊢ H ⊆ X
59 ssfi ⊢ X ∈ Fin ∧ H ⊆ X → H ∈ Fin
60 3 58 59 sylancl ⊢ φ → H ∈ Fin
61 hashnncl ⊢ H ∈ Fin → H ∈ ℕ ↔ H ≠ ∅
62 60 61 syl ⊢ φ → H ∈ ℕ ↔ H ≠ ∅
63 57 62 mpbird ⊢ φ → H ∈ ℕ
64 63 nnzd ⊢ φ → H ∈ ℤ
65 63 nnne0d ⊢ φ → H ≠ 0
66 pcmul ⊢ P ∈ ℙ ∧ B ∼ ˙ ∈ ℤ ∧ B ∼ ˙ ≠ 0 ∧ H ∈ ℤ ∧ H ≠ 0 → P pCnt B ∼ ˙ ⁢ H = P pCnt B ∼ ˙ + P pCnt H
67 4 52 53 64 65 66 syl122anc ⊢ φ → P pCnt B ∼ ˙ ⁢ H = P pCnt B ∼ ˙ + P pCnt H
68 51 67 eqtrd ⊢ φ → P pCnt X = P pCnt B ∼ ˙ + P pCnt H
69 47 68 breqtrd ⊢ φ → P pCnt B ∼ ˙ + N ≤ P pCnt B ∼ ˙ + P pCnt H
70 4 63 pccld ⊢ φ → P pCnt H ∈ ℕ 0
71 70 nn0red ⊢ φ → P pCnt H ∈ ℝ
72 37 71 36 leadd2d ⊢ φ → N ≤ P pCnt H ↔ P pCnt B ∼ ˙ + N ≤ P pCnt B ∼ ˙ + P pCnt H
73 69 72 mpbird ⊢ φ → N ≤ P pCnt H
74 pcdvdsb ⊢ P ∈ ℙ ∧ H ∈ ℤ ∧ N ∈ ℕ 0 → N ≤ P pCnt H ↔ P N ∥ H
75 4 64 5 74 syl3anc ⊢ φ → N ≤ P pCnt H ↔ P N ∥ H
76 73 75 mpbid ⊢ φ → P N ∥ H
77 prmnn ⊢ P ∈ ℙ → P ∈ ℕ
78 4 77 syl ⊢ φ → P ∈ ℕ
79 78 5 nnexpcld ⊢ φ → P N ∈ ℕ
80 79 nnzd ⊢ φ → P N ∈ ℤ
81 dvdsle ⊢ P N ∈ ℤ ∧ H ∈ ℕ → P N ∥ H → P N ≤ H
82 80 63 81 syl2anc ⊢ φ → P N ∥ H → P N ≤ H
83 76 82 mpd ⊢ φ → P N ≤ H
84 hashcl ⊢ H ∈ Fin → H ∈ ℕ 0
85 60 84 syl ⊢ φ → H ∈ ℕ 0
86 85 nn0red ⊢ φ → H ∈ ℝ
87 79 nnred ⊢ φ → P N ∈ ℝ
88 86 87 letri3d ⊢ φ → H = P N ↔ H ≤ P N ∧ P N ≤ H
89 17 83 88 mpbir2and ⊢ φ → H = P N
90 fveqeq2 ⊢ h = H → h = P N ↔ H = P N
91 90 rspcev ⊢ H ∈ SubGrp ⁡ G ∧ H = P N → ∃ h ∈ SubGrp ⁡ G h = P N
92 16 89 91 syl2anc ⊢ φ → ∃ h ∈ SubGrp ⁡ G h = P N