Step | Hyp | Ref
| Expression |
1 | | fislw.1 |
. . 3
⊢ 𝑋 = (Base‘𝐺) |
2 | | slwhash.4 |
. . . . 5
⊢ (𝜑 → 𝐻 ∈ (𝑃 pSyl 𝐺)) |
3 | | slwsubg 18025 |
. . . . 5
⊢ (𝐻 ∈ (𝑃 pSyl 𝐺) → 𝐻 ∈ (SubGrp‘𝐺)) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝐺)) |
5 | | subgrcl 17599 |
. . . 4
⊢ (𝐻 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺 ∈ Grp) |
7 | | slwhash.3 |
. . 3
⊢ (𝜑 → 𝑋 ∈ Fin) |
8 | | slwprm 18024 |
. . . 4
⊢ (𝐻 ∈ (𝑃 pSyl 𝐺) → 𝑃 ∈ ℙ) |
9 | 2, 8 | syl 17 |
. . 3
⊢ (𝜑 → 𝑃 ∈ ℙ) |
10 | 1 | grpbn0 17451 |
. . . . . 6
⊢ (𝐺 ∈ Grp → 𝑋 ≠ ∅) |
11 | 6, 10 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑋 ≠ ∅) |
12 | | hashnncl 13157 |
. . . . . 6
⊢ (𝑋 ∈ Fin →
((#‘𝑋) ∈ ℕ
↔ 𝑋 ≠
∅)) |
13 | 7, 12 | syl 17 |
. . . . 5
⊢ (𝜑 → ((#‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅)) |
14 | 11, 13 | mpbird 247 |
. . . 4
⊢ (𝜑 → (#‘𝑋) ∈ ℕ) |
15 | 9, 14 | pccld 15555 |
. . 3
⊢ (𝜑 → (𝑃 pCnt (#‘𝑋)) ∈
ℕ0) |
16 | | pcdvds 15568 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧
(#‘𝑋) ∈ ℕ)
→ (𝑃↑(𝑃 pCnt (#‘𝑋))) ∥ (#‘𝑋)) |
17 | 9, 14, 16 | syl2anc 693 |
. . 3
⊢ (𝜑 → (𝑃↑(𝑃 pCnt (#‘𝑋))) ∥ (#‘𝑋)) |
18 | 1, 6, 7, 9, 15, 17 | sylow1 18018 |
. 2
⊢ (𝜑 → ∃𝑘 ∈ (SubGrp‘𝐺)(#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋)))) |
19 | 7 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) → 𝑋 ∈ Fin) |
20 | 4 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) → 𝐻 ∈ (SubGrp‘𝐺)) |
21 | | simprl 794 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) → 𝑘 ∈ (SubGrp‘𝐺)) |
22 | | eqid 2622 |
. . . 4
⊢
(+g‘𝐺) = (+g‘𝐺) |
23 | | eqid 2622 |
. . . . . . 7
⊢ (𝐺 ↾s 𝐻) = (𝐺 ↾s 𝐻) |
24 | 23 | slwpgp 18028 |
. . . . . 6
⊢ (𝐻 ∈ (𝑃 pSyl 𝐺) → 𝑃 pGrp (𝐺 ↾s 𝐻)) |
25 | 2, 24 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾s 𝐻)) |
26 | 25 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) → 𝑃 pGrp (𝐺 ↾s 𝐻)) |
27 | | simprr 796 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) → (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋)))) |
28 | | eqid 2622 |
. . . 4
⊢
(-g‘𝐺) = (-g‘𝐺) |
29 | 1, 19, 20, 21, 22, 26, 27, 28 | sylow2b 18038 |
. . 3
⊢ ((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))) |
30 | | simprr 796 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))) |
31 | 2 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → 𝐻 ∈ (𝑃 pSyl 𝐺)) |
32 | 31, 8 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → 𝑃 ∈ ℙ) |
33 | 15 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → (𝑃 pCnt (#‘𝑋)) ∈
ℕ0) |
34 | 21 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → 𝑘 ∈ (SubGrp‘𝐺)) |
35 | | simprl 794 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → 𝑔 ∈ 𝑋) |
36 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)) = (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)) |
37 | 1, 22, 28, 36 | conjsubg 17692 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ (SubGrp‘𝐺) ∧ 𝑔 ∈ 𝑋) → ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)) ∈ (SubGrp‘𝐺)) |
38 | 34, 35, 37 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)) ∈ (SubGrp‘𝐺)) |
39 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝐺 ↾s ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))) = (𝐺 ↾s ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))) |
40 | 39 | subgbas 17598 |
. . . . . . . . . . 11
⊢ (ran
(𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)) ∈ (SubGrp‘𝐺) → ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)) = (Base‘(𝐺 ↾s ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))))) |
41 | 38, 40 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)) = (Base‘(𝐺 ↾s ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))))) |
42 | 41 | fveq2d 6195 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → (#‘ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))) = (#‘(Base‘(𝐺 ↾s ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))))) |
43 | 1, 22, 28, 36 | conjsubgen 17693 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ (SubGrp‘𝐺) ∧ 𝑔 ∈ 𝑋) → 𝑘 ≈ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))) |
44 | 34, 35, 43 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → 𝑘 ≈ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))) |
45 | 7 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → 𝑋 ∈ Fin) |
46 | 1 | subgss 17595 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (SubGrp‘𝐺) → 𝑘 ⊆ 𝑋) |
47 | 34, 46 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → 𝑘 ⊆ 𝑋) |
48 | | ssfi 8180 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ Fin ∧ 𝑘 ⊆ 𝑋) → 𝑘 ∈ Fin) |
49 | 45, 47, 48 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → 𝑘 ∈ Fin) |
50 | 1 | subgss 17595 |
. . . . . . . . . . . . . 14
⊢ (ran
(𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)) ∈ (SubGrp‘𝐺) → ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)) ⊆ 𝑋) |
51 | 38, 50 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)) ⊆ 𝑋) |
52 | | ssfi 8180 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ Fin ∧ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)) ⊆ 𝑋) → ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)) ∈ Fin) |
53 | 45, 51, 52 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)) ∈ Fin) |
54 | | hashen 13135 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ Fin ∧ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)) ∈ Fin) → ((#‘𝑘) = (#‘ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))) ↔ 𝑘 ≈ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) |
55 | 49, 53, 54 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → ((#‘𝑘) = (#‘ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))) ↔ 𝑘 ≈ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) |
56 | 44, 55 | mpbird 247 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → (#‘𝑘) = (#‘ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) |
57 | | simplrr 801 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋)))) |
58 | 56, 57 | eqtr3d 2658 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → (#‘ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))) = (𝑃↑(𝑃 pCnt (#‘𝑋)))) |
59 | 42, 58 | eqtr3d 2658 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → (#‘(Base‘(𝐺 ↾s ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))))) = (𝑃↑(𝑃 pCnt (#‘𝑋)))) |
60 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑃 pCnt (#‘𝑋)) → (𝑃↑𝑛) = (𝑃↑(𝑃 pCnt (#‘𝑋)))) |
61 | 60 | eqeq2d 2632 |
. . . . . . . . 9
⊢ (𝑛 = (𝑃 pCnt (#‘𝑋)) → ((#‘(Base‘(𝐺 ↾s ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))))) = (𝑃↑𝑛) ↔ (#‘(Base‘(𝐺 ↾s ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))))) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) |
62 | 61 | rspcev 3309 |
. . . . . . . 8
⊢ (((𝑃 pCnt (#‘𝑋)) ∈ ℕ0 ∧
(#‘(Base‘(𝐺
↾s ran (𝑥
∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))))) = (𝑃↑(𝑃 pCnt (#‘𝑋)))) → ∃𝑛 ∈ ℕ0
(#‘(Base‘(𝐺
↾s ran (𝑥
∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))))) = (𝑃↑𝑛)) |
63 | 33, 59, 62 | syl2anc 693 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → ∃𝑛 ∈ ℕ0
(#‘(Base‘(𝐺
↾s ran (𝑥
∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))))) = (𝑃↑𝑛)) |
64 | 39 | subggrp 17597 |
. . . . . . . . 9
⊢ (ran
(𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)) ∈ (SubGrp‘𝐺) → (𝐺 ↾s ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))) ∈ Grp) |
65 | 38, 64 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → (𝐺 ↾s ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))) ∈ Grp) |
66 | 41, 53 | eqeltrrd 2702 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → (Base‘(𝐺 ↾s ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) ∈ Fin) |
67 | | eqid 2622 |
. . . . . . . . 9
⊢
(Base‘(𝐺
↾s ran (𝑥
∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) = (Base‘(𝐺 ↾s ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) |
68 | 67 | pgpfi 18020 |
. . . . . . . 8
⊢ (((𝐺 ↾s ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))) ∈ Grp ∧ (Base‘(𝐺 ↾s ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) ∈ Fin) → (𝑃 pGrp (𝐺 ↾s ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))) ↔ (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0
(#‘(Base‘(𝐺
↾s ran (𝑥
∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))))) = (𝑃↑𝑛)))) |
69 | 65, 66, 68 | syl2anc 693 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → (𝑃 pGrp (𝐺 ↾s ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))) ↔ (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0
(#‘(Base‘(𝐺
↾s ran (𝑥
∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))))) = (𝑃↑𝑛)))) |
70 | 32, 63, 69 | mpbir2and 957 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → 𝑃 pGrp (𝐺 ↾s ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) |
71 | 39 | slwispgp 18026 |
. . . . . . 7
⊢ ((𝐻 ∈ (𝑃 pSyl 𝐺) ∧ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)) ∈ (SubGrp‘𝐺)) → ((𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)) ∧ 𝑃 pGrp (𝐺 ↾s ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) ↔ 𝐻 = ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) |
72 | 31, 38, 71 | syl2anc 693 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → ((𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)) ∧ 𝑃 pGrp (𝐺 ↾s ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) ↔ 𝐻 = ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) |
73 | 30, 70, 72 | mpbi2and 956 |
. . . . 5
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → 𝐻 = ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔))) |
74 | 73 | fveq2d 6195 |
. . . 4
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → (#‘𝐻) = (#‘ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) |
75 | 74, 58 | eqtrd 2656 |
. . 3
⊢ (((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) ∧ (𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran (𝑥 ∈ 𝑘 ↦ ((𝑔(+g‘𝐺)𝑥)(-g‘𝐺)𝑔)))) → (#‘𝐻) = (𝑃↑(𝑃 pCnt (#‘𝑋)))) |
76 | 29, 75 | rexlimddv 3035 |
. 2
⊢ ((𝜑 ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (#‘𝑘) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) → (#‘𝐻) = (𝑃↑(𝑃 pCnt (#‘𝑋)))) |
77 | 18, 76 | rexlimddv 3035 |
1
⊢ (𝜑 → (#‘𝐻) = (𝑃↑(𝑃 pCnt (#‘𝑋)))) |