Metamath Proof Explorer

Theorem slwhash

Description: A sylow subgroup has cardinality equal to the maximum power of P dividing the group. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypotheses fislw.1 ⊢ X = Base G
slwhash.3 ⊢ φ → X ∈ Fin
slwhash.4 ⊢ φ → H ∈ P pSyl G
Assertion slwhash ⊢ φ → H = P P pCnt X

Proof

Step Hyp Ref Expression
1 fislw.1 ⊢ X = Base G
2 slwhash.3 ⊢ φ → X ∈ Fin
3 slwhash.4 ⊢ φ → H ∈ P pSyl G
4 slwsubg ⊢ H ∈ P pSyl G → H ∈ SubGrp ⁡ G
5 3 4 syl ⊢ φ → H ∈ SubGrp ⁡ G
6 subgrcl ⊢ H ∈ SubGrp ⁡ G → G ∈ Grp
7 5 6 syl ⊢ φ → G ∈ Grp
8 slwprm ⊢ H ∈ P pSyl G → P ∈ ℙ
9 3 8 syl ⊢ φ → P ∈ ℙ
10 1 grpbn0 ⊢ G ∈ Grp → X ≠ ∅
11 7 10 syl ⊢ φ → X ≠ ∅
12 hashnncl ⊢ X ∈ Fin → X ∈ ℕ ↔ X ≠ ∅
13 2 12 syl ⊢ φ → X ∈ ℕ ↔ X ≠ ∅
14 11 13 mpbird ⊢ φ → X ∈ ℕ
15 9 14 pccld ⊢ φ → P pCnt X ∈ ℕ 0
16 pcdvds ⊢ P ∈ ℙ ∧ X ∈ ℕ → P P pCnt X ∥ X
17 9 14 16 syl2anc ⊢ φ → P P pCnt X ∥ X
18 1 7 2 9 15 17 sylow1 ⊢ φ → ∃ k ∈ SubGrp ⁡ G k = P P pCnt X
19 2 adantr ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X → X ∈ Fin
20 5 adantr ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X → H ∈ SubGrp ⁡ G
21 simprl ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X → k ∈ SubGrp ⁡ G
22 eqid ⊢ + G = + G
23 eqid ⊢ G ↾ 𝑠 H = G ↾ 𝑠 H
24 23 slwpgp ⊢ H ∈ P pSyl G → P pGrp G ↾ 𝑠 H
25 3 24 syl ⊢ φ → P pGrp G ↾ 𝑠 H
26 25 adantr ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X → P pGrp G ↾ 𝑠 H
27 simprr ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X → k = P P pCnt X
28 eqid ⊢ - G = - G
29 1 19 20 21 22 26 27 28 sylow2b ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X → ∃ g ∈ X H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g
30 simprr ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g
31 3 ad2antrr ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → H ∈ P pSyl G
32 31 8 syl ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → P ∈ ℙ
33 15 ad2antrr ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → P pCnt X ∈ ℕ 0
34 21 adantr ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → k ∈ SubGrp ⁡ G
35 simprl ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → g ∈ X
36 eqid ⊢ x ∈ k ⟼ g + G x - G g = x ∈ k ⟼ g + G x - G g
37 1 22 28 36 conjsubg ⊢ k ∈ SubGrp ⁡ G ∧ g ∈ X → ran ⁡ x ∈ k ⟼ g + G x - G g ∈ SubGrp ⁡ G
38 34 35 37 syl2anc ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → ran ⁡ x ∈ k ⟼ g + G x - G g ∈ SubGrp ⁡ G
39 eqid ⊢ G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g = G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g
40 39 subgbas ⊢ ran ⁡ x ∈ k ⟼ g + G x - G g ∈ SubGrp ⁡ G → ran ⁡ x ∈ k ⟼ g + G x - G g = Base G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g
41 38 40 syl ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → ran ⁡ x ∈ k ⟼ g + G x - G g = Base G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g
42 41 fveq2d ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → ran ⁡ x ∈ k ⟼ g + G x - G g = Base G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g
43 1 22 28 36 conjsubgen ⊢ k ∈ SubGrp ⁡ G ∧ g ∈ X → k ≈ ran ⁡ x ∈ k ⟼ g + G x - G g
44 34 35 43 syl2anc ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → k ≈ ran ⁡ x ∈ k ⟼ g + G x - G g
45 2 ad2antrr ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → X ∈ Fin
46 1 subgss ⊢ k ∈ SubGrp ⁡ G → k ⊆ X
47 34 46 syl ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → k ⊆ X
48 45 47 ssfid ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → k ∈ Fin
49 1 subgss ⊢ ran ⁡ x ∈ k ⟼ g + G x - G g ∈ SubGrp ⁡ G → ran ⁡ x ∈ k ⟼ g + G x - G g ⊆ X
50 38 49 syl ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → ran ⁡ x ∈ k ⟼ g + G x - G g ⊆ X
51 45 50 ssfid ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → ran ⁡ x ∈ k ⟼ g + G x - G g ∈ Fin
52 hashen ⊢ k ∈ Fin ∧ ran ⁡ x ∈ k ⟼ g + G x - G g ∈ Fin → k = ran ⁡ x ∈ k ⟼ g + G x - G g ↔ k ≈ ran ⁡ x ∈ k ⟼ g + G x - G g
53 48 51 52 syl2anc ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → k = ran ⁡ x ∈ k ⟼ g + G x - G g ↔ k ≈ ran ⁡ x ∈ k ⟼ g + G x - G g
54 44 53 mpbird ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → k = ran ⁡ x ∈ k ⟼ g + G x - G g
55 simplrr ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → k = P P pCnt X
56 54 55 eqtr3d ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → ran ⁡ x ∈ k ⟼ g + G x - G g = P P pCnt X
57 42 56 eqtr3d ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → Base G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g = P P pCnt X
58 oveq2 ⊢ n = P pCnt X → P n = P P pCnt X
59 58 rspceeqv ⊢ P pCnt X ∈ ℕ 0 ∧ Base G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g = P P pCnt X → ∃ n ∈ ℕ 0 Base G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g = P n
60 33 57 59 syl2anc ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → ∃ n ∈ ℕ 0 Base G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g = P n
61 39 subggrp ⊢ ran ⁡ x ∈ k ⟼ g + G x - G g ∈ SubGrp ⁡ G → G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g ∈ Grp
62 38 61 syl ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g ∈ Grp
63 41 51 eqeltrrd ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → Base G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g ∈ Fin
64 eqid ⊢ Base G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g = Base G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g
65 64 pgpfi ⊢ G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g ∈ Grp ∧ Base G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g ∈ Fin → P pGrp G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g ↔ P ∈ ℙ ∧ ∃ n ∈ ℕ 0 Base G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g = P n
66 62 63 65 syl2anc ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → P pGrp G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g ↔ P ∈ ℙ ∧ ∃ n ∈ ℕ 0 Base G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g = P n
67 32 60 66 mpbir2and ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → P pGrp G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g
68 39 slwispgp ⊢ H ∈ P pSyl G ∧ ran ⁡ x ∈ k ⟼ g + G x - G g ∈ SubGrp ⁡ G → H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g ∧ P pGrp G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g ↔ H = ran ⁡ x ∈ k ⟼ g + G x - G g
69 31 38 68 syl2anc ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g ∧ P pGrp G ↾ 𝑠 ran ⁡ x ∈ k ⟼ g + G x - G g ↔ H = ran ⁡ x ∈ k ⟼ g + G x - G g
70 30 67 69 mpbi2and ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → H = ran ⁡ x ∈ k ⟼ g + G x - G g
71 70 fveq2d ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → H = ran ⁡ x ∈ k ⟼ g + G x - G g
72 71 56 eqtrd ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X ∧ g ∈ X ∧ H ⊆ ran ⁡ x ∈ k ⟼ g + G x - G g → H = P P pCnt X
73 29 72 rexlimddv ⊢ φ ∧ k ∈ SubGrp ⁡ G ∧ k = P P pCnt X → H = P P pCnt X
74 18 73 rexlimddv ⊢ φ → H = P P pCnt X