Step | Hyp | Ref
| Expression |
1 | | simpr 480 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝐻 ∈ (𝑃 pSyl 𝐺)) → 𝐻 ∈ (𝑃 pSyl 𝐺)) |
2 | | slwsubg 18238 |
. . . 4
⊢ (𝐻 ∈ (𝑃 pSyl 𝐺) → 𝐻 ∈ (SubGrp‘𝐺)) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝐻 ∈ (𝑃 pSyl 𝐺)) → 𝐻 ∈ (SubGrp‘𝐺)) |
4 | | fislw.1 |
. . . 4
⊢ 𝑋 = (Base‘𝐺) |
5 | | simpl2 1227 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝐻 ∈ (𝑃 pSyl 𝐺)) → 𝑋 ∈ Fin) |
6 | 4, 5, 1 | slwhash 18252 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝐻 ∈ (𝑃 pSyl 𝐺)) → (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋)))) |
7 | 3, 6 | jca 556 |
. 2
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝐻 ∈ (𝑃 pSyl 𝐺)) → (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) |
8 | | simpl3 1229 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → 𝑃 ∈ ℙ) |
9 | | simprl 808 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → 𝐻 ∈ (SubGrp‘𝐺)) |
10 | | simpl2 1227 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → 𝑋 ∈ Fin) |
11 | 10 | adantr 473 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑋 ∈ Fin) |
12 | | simprl 808 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑘 ∈ (SubGrp‘𝐺)) |
13 | 4 | subgss 17809 |
. . . . . . . . 9
⊢ (𝑘 ∈ (SubGrp‘𝐺) → 𝑘 ⊆ 𝑋) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑘 ⊆ 𝑋) |
15 | | ssfi 8334 |
. . . . . . . 8
⊢ ((𝑋 ∈ Fin ∧ 𝑘 ⊆ 𝑋) → 𝑘 ∈ Fin) |
16 | 11, 14, 15 | syl2anc 693 |
. . . . . . 7
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑘 ∈ Fin) |
17 | | simprrl 820 |
. . . . . . 7
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝐻 ⊆ 𝑘) |
18 | | ssdomg 8153 |
. . . . . . . . 9
⊢ (𝑘 ∈ Fin → (𝐻 ⊆ 𝑘 → 𝐻 ≼ 𝑘)) |
19 | 16, 17, 18 | sylc 65 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝐻 ≼ 𝑘) |
20 | | simprrr 821 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑃 pGrp (𝐺 ↾s 𝑘)) |
21 | | eqid 2769 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ↾s 𝑘) = (𝐺 ↾s 𝑘) |
22 | 21 | subggrp 17811 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (SubGrp‘𝐺) → (𝐺 ↾s 𝑘) ∈ Grp) |
23 | 12, 22 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (𝐺 ↾s 𝑘) ∈ Grp) |
24 | 21 | subgbas 17812 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (SubGrp‘𝐺) → 𝑘 = (Base‘(𝐺 ↾s 𝑘))) |
25 | 12, 24 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑘 = (Base‘(𝐺 ↾s 𝑘))) |
26 | 25, 16 | eqeltrrd 2849 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (Base‘(𝐺 ↾s 𝑘)) ∈ Fin) |
27 | | eqid 2769 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘(𝐺
↾s 𝑘)) =
(Base‘(𝐺
↾s 𝑘)) |
28 | 27 | pgpfi 18233 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ↾s 𝑘) ∈ Grp ∧
(Base‘(𝐺
↾s 𝑘))
∈ Fin) → (𝑃 pGrp
(𝐺 ↾s
𝑘) ↔ (𝑃 ∈ ℙ ∧
∃𝑛 ∈
ℕ0 (♯‘(Base‘(𝐺 ↾s 𝑘))) = (𝑃↑𝑛)))) |
29 | 23, 26, 28 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (𝑃 pGrp (𝐺 ↾s 𝑘) ↔ (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0
(♯‘(Base‘(𝐺 ↾s 𝑘))) = (𝑃↑𝑛)))) |
30 | 20, 29 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0
(♯‘(Base‘(𝐺 ↾s 𝑘))) = (𝑃↑𝑛))) |
31 | 30 | simpld 478 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑃 ∈ ℙ) |
32 | | prmnn 15601 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑃 ∈ ℕ) |
34 | 33 | nnred 11235 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑃 ∈ ℝ) |
35 | 33 | nnge1d 11263 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 1 ≤ 𝑃) |
36 | | eqid 2769 |
. . . . . . . . . . . . . . . . . 18
⊢
(0g‘𝐺) = (0g‘𝐺) |
37 | 36 | subg0cl 17816 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝑘) |
38 | 12, 37 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (0g‘𝐺) ∈ 𝑘) |
39 | | ne0i 4066 |
. . . . . . . . . . . . . . . 16
⊢
((0g‘𝐺) ∈ 𝑘 → 𝑘 ≠ ∅) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑘 ≠ ∅) |
41 | | hashnncl 13362 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ Fin →
((♯‘𝑘) ∈
ℕ ↔ 𝑘 ≠
∅)) |
42 | 16, 41 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → ((♯‘𝑘) ∈ ℕ ↔ 𝑘 ≠ ∅)) |
43 | 40, 42 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (♯‘𝑘) ∈ ℕ) |
44 | 31, 43 | pccld 15768 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (𝑃 pCnt (♯‘𝑘)) ∈
ℕ0) |
45 | 44 | nn0zd 11680 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (𝑃 pCnt (♯‘𝑘)) ∈ ℤ) |
46 | | simpl1 1225 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → 𝐺 ∈ Grp) |
47 | 4 | grpbn0 17665 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ Grp → 𝑋 ≠ ∅) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → 𝑋 ≠ ∅) |
49 | | hashnncl 13362 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ Fin →
((♯‘𝑋) ∈
ℕ ↔ 𝑋 ≠
∅)) |
50 | 10, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅)) |
51 | 48, 50 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → (♯‘𝑋) ∈
ℕ) |
52 | 8, 51 | pccld 15768 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → (𝑃 pCnt (♯‘𝑋)) ∈
ℕ0) |
53 | 52 | adantr 473 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (𝑃 pCnt (♯‘𝑋)) ∈
ℕ0) |
54 | 53 | nn0zd 11680 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (𝑃 pCnt (♯‘𝑋)) ∈ ℤ) |
55 | | oveq1 6798 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑃 → (𝑝 pCnt (♯‘𝑘)) = (𝑃 pCnt (♯‘𝑘))) |
56 | | oveq1 6798 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑃 → (𝑝 pCnt (♯‘𝑋)) = (𝑃 pCnt (♯‘𝑋))) |
57 | 55, 56 | breq12d 4796 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑃 → ((𝑝 pCnt (♯‘𝑘)) ≤ (𝑝 pCnt (♯‘𝑋)) ↔ (𝑃 pCnt (♯‘𝑘)) ≤ (𝑃 pCnt (♯‘𝑋)))) |
58 | 4 | lagsubg 17870 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin) → (♯‘𝑘) ∥ (♯‘𝑋)) |
59 | 12, 11, 58 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (♯‘𝑘) ∥ (♯‘𝑋)) |
60 | 43 | nnzd 11681 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (♯‘𝑘) ∈ ℤ) |
61 | 51 | adantr 473 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (♯‘𝑋) ∈ ℕ) |
62 | 61 | nnzd 11681 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (♯‘𝑋) ∈ ℤ) |
63 | | pc2dvds 15796 |
. . . . . . . . . . . . . . 15
⊢
(((♯‘𝑘)
∈ ℤ ∧ (♯‘𝑋) ∈ ℤ) →
((♯‘𝑘) ∥
(♯‘𝑋) ↔
∀𝑝 ∈ ℙ
(𝑝 pCnt
(♯‘𝑘)) ≤
(𝑝 pCnt
(♯‘𝑋)))) |
64 | 60, 62, 63 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → ((♯‘𝑘) ∥ (♯‘𝑋) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (♯‘𝑘)) ≤ (𝑝 pCnt (♯‘𝑋)))) |
65 | 59, 64 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → ∀𝑝 ∈ ℙ (𝑝 pCnt (♯‘𝑘)) ≤ (𝑝 pCnt (♯‘𝑋))) |
66 | 57, 65, 31 | rspcdva 3463 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (𝑃 pCnt (♯‘𝑘)) ≤ (𝑃 pCnt (♯‘𝑋))) |
67 | | eluz2 11893 |
. . . . . . . . . . . 12
⊢ ((𝑃 pCnt (♯‘𝑋)) ∈
(ℤ≥‘(𝑃 pCnt (♯‘𝑘))) ↔ ((𝑃 pCnt (♯‘𝑘)) ∈ ℤ ∧ (𝑃 pCnt (♯‘𝑋)) ∈ ℤ ∧ (𝑃 pCnt (♯‘𝑘)) ≤ (𝑃 pCnt (♯‘𝑋)))) |
68 | 45, 54, 66, 67 | syl3anbrc 1426 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (𝑃 pCnt (♯‘𝑋)) ∈
(ℤ≥‘(𝑃 pCnt (♯‘𝑘)))) |
69 | 34, 35, 68 | leexp2ad 13248 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (𝑃↑(𝑃 pCnt (♯‘𝑘))) ≤ (𝑃↑(𝑃 pCnt (♯‘𝑋)))) |
70 | 30 | simprd 483 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → ∃𝑛 ∈ ℕ0
(♯‘(Base‘(𝐺 ↾s 𝑘))) = (𝑃↑𝑛)) |
71 | 25 | fveq2d 6335 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (♯‘𝑘) = (♯‘(Base‘(𝐺 ↾s 𝑘)))) |
72 | 71 | eqeq1d 2771 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → ((♯‘𝑘) = (𝑃↑𝑛) ↔ (♯‘(Base‘(𝐺 ↾s 𝑘))) = (𝑃↑𝑛))) |
73 | 72 | rexbidv 3198 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (∃𝑛 ∈ ℕ0
(♯‘𝑘) = (𝑃↑𝑛) ↔ ∃𝑛 ∈ ℕ0
(♯‘(Base‘(𝐺 ↾s 𝑘))) = (𝑃↑𝑛))) |
74 | 70, 73 | mpbird 247 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → ∃𝑛 ∈ ℕ0
(♯‘𝑘) = (𝑃↑𝑛)) |
75 | | pcprmpw 15800 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧
(♯‘𝑘) ∈
ℕ) → (∃𝑛
∈ ℕ0 (♯‘𝑘) = (𝑃↑𝑛) ↔ (♯‘𝑘) = (𝑃↑(𝑃 pCnt (♯‘𝑘))))) |
76 | 31, 43, 75 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (∃𝑛 ∈ ℕ0
(♯‘𝑘) = (𝑃↑𝑛) ↔ (♯‘𝑘) = (𝑃↑(𝑃 pCnt (♯‘𝑘))))) |
77 | 74, 76 | mpbid 222 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (♯‘𝑘) = (𝑃↑(𝑃 pCnt (♯‘𝑘)))) |
78 | | simplrr 817 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋)))) |
79 | 69, 77, 78 | 3brtr4d 4815 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (♯‘𝑘) ≤ (♯‘𝐻)) |
80 | 4 | subgss 17809 |
. . . . . . . . . . . . 13
⊢ (𝐻 ∈ (SubGrp‘𝐺) → 𝐻 ⊆ 𝑋) |
81 | 80 | ad2antrl 763 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → 𝐻 ⊆ 𝑋) |
82 | | ssfi 8334 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ Fin ∧ 𝐻 ⊆ 𝑋) → 𝐻 ∈ Fin) |
83 | 10, 81, 82 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → 𝐻 ∈ Fin) |
84 | 83 | adantr 473 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝐻 ∈ Fin) |
85 | | hashdom 13373 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ Fin ∧ 𝐻 ∈ Fin) →
((♯‘𝑘) ≤
(♯‘𝐻) ↔
𝑘 ≼ 𝐻)) |
86 | 16, 84, 85 | syl2anc 693 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → ((♯‘𝑘) ≤ (♯‘𝐻) ↔ 𝑘 ≼ 𝐻)) |
87 | 79, 86 | mpbid 222 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑘 ≼ 𝐻) |
88 | | sbth 8234 |
. . . . . . . 8
⊢ ((𝐻 ≼ 𝑘 ∧ 𝑘 ≼ 𝐻) → 𝐻 ≈ 𝑘) |
89 | 19, 87, 88 | syl2anc 693 |
. . . . . . 7
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝐻 ≈ 𝑘) |
90 | | fisseneq 8325 |
. . . . . . 7
⊢ ((𝑘 ∈ Fin ∧ 𝐻 ⊆ 𝑘 ∧ 𝐻 ≈ 𝑘) → 𝐻 = 𝑘) |
91 | 16, 17, 89, 90 | syl3anc 1474 |
. . . . . 6
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝐻 = 𝑘) |
92 | 91 | expr 641 |
. . . . 5
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ 𝑘 ∈ (SubGrp‘𝐺)) → ((𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)) → 𝐻 = 𝑘)) |
93 | | eqid 2769 |
. . . . . . . . . . . . 13
⊢ (𝐺 ↾s 𝐻) = (𝐺 ↾s 𝐻) |
94 | 93 | subgbas 17812 |
. . . . . . . . . . . 12
⊢ (𝐻 ∈ (SubGrp‘𝐺) → 𝐻 = (Base‘(𝐺 ↾s 𝐻))) |
95 | 94 | ad2antrl 763 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → 𝐻 = (Base‘(𝐺 ↾s 𝐻))) |
96 | 95 | fveq2d 6335 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → (♯‘𝐻) =
(♯‘(Base‘(𝐺 ↾s 𝐻)))) |
97 | | simprr 810 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋)))) |
98 | 96, 97 | eqtr3d 2805 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) →
(♯‘(Base‘(𝐺 ↾s 𝐻))) = (𝑃↑(𝑃 pCnt (♯‘𝑋)))) |
99 | | oveq2 6799 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑃 pCnt (♯‘𝑋)) → (𝑃↑𝑛) = (𝑃↑(𝑃 pCnt (♯‘𝑋)))) |
100 | 99 | eqeq2d 2779 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑃 pCnt (♯‘𝑋)) → ((♯‘(Base‘(𝐺 ↾s 𝐻))) = (𝑃↑𝑛) ↔ (♯‘(Base‘(𝐺 ↾s 𝐻))) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) |
101 | 100 | rspcev 3457 |
. . . . . . . . 9
⊢ (((𝑃 pCnt (♯‘𝑋)) ∈ ℕ0
∧ (♯‘(Base‘(𝐺 ↾s 𝐻))) = (𝑃↑(𝑃 pCnt (♯‘𝑋)))) → ∃𝑛 ∈ ℕ0
(♯‘(Base‘(𝐺 ↾s 𝐻))) = (𝑃↑𝑛)) |
102 | 52, 98, 101 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → ∃𝑛 ∈ ℕ0
(♯‘(Base‘(𝐺 ↾s 𝐻))) = (𝑃↑𝑛)) |
103 | 93 | subggrp 17811 |
. . . . . . . . . 10
⊢ (𝐻 ∈ (SubGrp‘𝐺) → (𝐺 ↾s 𝐻) ∈ Grp) |
104 | 103 | ad2antrl 763 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → (𝐺 ↾s 𝐻) ∈ Grp) |
105 | 95, 83 | eqeltrrd 2849 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → (Base‘(𝐺 ↾s 𝐻)) ∈ Fin) |
106 | | eqid 2769 |
. . . . . . . . . 10
⊢
(Base‘(𝐺
↾s 𝐻)) =
(Base‘(𝐺
↾s 𝐻)) |
107 | 106 | pgpfi 18233 |
. . . . . . . . 9
⊢ (((𝐺 ↾s 𝐻) ∈ Grp ∧
(Base‘(𝐺
↾s 𝐻))
∈ Fin) → (𝑃 pGrp
(𝐺 ↾s
𝐻) ↔ (𝑃 ∈ ℙ ∧
∃𝑛 ∈
ℕ0 (♯‘(Base‘(𝐺 ↾s 𝐻))) = (𝑃↑𝑛)))) |
108 | 104, 105,
107 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → (𝑃 pGrp (𝐺 ↾s 𝐻) ↔ (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0
(♯‘(Base‘(𝐺 ↾s 𝐻))) = (𝑃↑𝑛)))) |
109 | 8, 102, 108 | mpbir2and 992 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → 𝑃 pGrp (𝐺 ↾s 𝐻)) |
110 | 109 | adantr 473 |
. . . . . 6
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ 𝑘 ∈ (SubGrp‘𝐺)) → 𝑃 pGrp (𝐺 ↾s 𝐻)) |
111 | | oveq2 6799 |
. . . . . . . 8
⊢ (𝐻 = 𝑘 → (𝐺 ↾s 𝐻) = (𝐺 ↾s 𝑘)) |
112 | 111 | breq2d 4795 |
. . . . . . 7
⊢ (𝐻 = 𝑘 → (𝑃 pGrp (𝐺 ↾s 𝐻) ↔ 𝑃 pGrp (𝐺 ↾s 𝑘))) |
113 | | eqimss 3803 |
. . . . . . . 8
⊢ (𝐻 = 𝑘 → 𝐻 ⊆ 𝑘) |
114 | 113 | biantrurd 531 |
. . . . . . 7
⊢ (𝐻 = 𝑘 → (𝑃 pGrp (𝐺 ↾s 𝑘) ↔ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) |
115 | 112, 114 | bitrd 268 |
. . . . . 6
⊢ (𝐻 = 𝑘 → (𝑃 pGrp (𝐺 ↾s 𝐻) ↔ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) |
116 | 110, 115 | syl5ibcom 235 |
. . . . 5
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ 𝑘 ∈ (SubGrp‘𝐺)) → (𝐻 = 𝑘 → (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) |
117 | 92, 116 | impbid 202 |
. . . 4
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ 𝑘 ∈ (SubGrp‘𝐺)) → ((𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)) ↔ 𝐻 = 𝑘)) |
118 | 117 | ralrimiva 3113 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → ∀𝑘 ∈ (SubGrp‘𝐺)((𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)) ↔ 𝐻 = 𝑘)) |
119 | | isslw 18236 |
. . 3
⊢ (𝐻 ∈ (𝑃 pSyl 𝐺) ↔ (𝑃 ∈ ℙ ∧ 𝐻 ∈ (SubGrp‘𝐺) ∧ ∀𝑘 ∈ (SubGrp‘𝐺)((𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)) ↔ 𝐻 = 𝑘))) |
120 | 8, 9, 118, 119 | syl3anbrc 1426 |
. 2
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → 𝐻 ∈ (𝑃 pSyl 𝐺)) |
121 | 7, 120 | impbida 910 |
1
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) → (𝐻 ∈ (𝑃 pSyl 𝐺) ↔ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋)))))) |