| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝐻 ∈ (𝑃 pSyl 𝐺)) → 𝐻 ∈ (𝑃 pSyl 𝐺)) |
| 2 | | slwsubg 19628 |
. . . 4
⊢ (𝐻 ∈ (𝑃 pSyl 𝐺) → 𝐻 ∈ (SubGrp‘𝐺)) |
| 3 | 1, 2 | syl 17 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝐻 ∈ (𝑃 pSyl 𝐺)) → 𝐻 ∈ (SubGrp‘𝐺)) |
| 4 | | fislw.1 |
. . . 4
⊢ 𝑋 = (Base‘𝐺) |
| 5 | | simpl2 1193 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝐻 ∈ (𝑃 pSyl 𝐺)) → 𝑋 ∈ Fin) |
| 6 | 4, 5, 1 | slwhash 19642 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝐻 ∈ (𝑃 pSyl 𝐺)) → (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋)))) |
| 7 | 3, 6 | jca 511 |
. 2
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝐻 ∈ (𝑃 pSyl 𝐺)) → (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) |
| 8 | | simpl3 1194 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → 𝑃 ∈ ℙ) |
| 9 | | simprl 771 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → 𝐻 ∈ (SubGrp‘𝐺)) |
| 10 | | simpl2 1193 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → 𝑋 ∈ Fin) |
| 11 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑋 ∈ Fin) |
| 12 | | simprl 771 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑘 ∈ (SubGrp‘𝐺)) |
| 13 | 4 | subgss 19145 |
. . . . . . . . 9
⊢ (𝑘 ∈ (SubGrp‘𝐺) → 𝑘 ⊆ 𝑋) |
| 14 | 12, 13 | syl 17 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑘 ⊆ 𝑋) |
| 15 | 11, 14 | ssfid 9301 |
. . . . . . 7
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑘 ∈ Fin) |
| 16 | | simprrl 781 |
. . . . . . 7
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝐻 ⊆ 𝑘) |
| 17 | | ssdomg 9040 |
. . . . . . . . 9
⊢ (𝑘 ∈ Fin → (𝐻 ⊆ 𝑘 → 𝐻 ≼ 𝑘)) |
| 18 | 15, 16, 17 | sylc 65 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝐻 ≼ 𝑘) |
| 19 | | simprrr 782 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑃 pGrp (𝐺 ↾s 𝑘)) |
| 20 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ↾s 𝑘) = (𝐺 ↾s 𝑘) |
| 21 | 20 | subggrp 19147 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (SubGrp‘𝐺) → (𝐺 ↾s 𝑘) ∈ Grp) |
| 22 | 12, 21 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (𝐺 ↾s 𝑘) ∈ Grp) |
| 23 | 20 | subgbas 19148 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (SubGrp‘𝐺) → 𝑘 = (Base‘(𝐺 ↾s 𝑘))) |
| 24 | 12, 23 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑘 = (Base‘(𝐺 ↾s 𝑘))) |
| 25 | 24, 15 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (Base‘(𝐺 ↾s 𝑘)) ∈ Fin) |
| 26 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘(𝐺
↾s 𝑘)) =
(Base‘(𝐺
↾s 𝑘)) |
| 27 | 26 | pgpfi 19623 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ↾s 𝑘) ∈ Grp ∧
(Base‘(𝐺
↾s 𝑘))
∈ Fin) → (𝑃 pGrp
(𝐺 ↾s
𝑘) ↔ (𝑃 ∈ ℙ ∧
∃𝑛 ∈
ℕ0 (♯‘(Base‘(𝐺 ↾s 𝑘))) = (𝑃↑𝑛)))) |
| 28 | 22, 25, 27 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (𝑃 pGrp (𝐺 ↾s 𝑘) ↔ (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0
(♯‘(Base‘(𝐺 ↾s 𝑘))) = (𝑃↑𝑛)))) |
| 29 | 19, 28 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0
(♯‘(Base‘(𝐺 ↾s 𝑘))) = (𝑃↑𝑛))) |
| 30 | 29 | simpld 494 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑃 ∈ ℙ) |
| 31 | | prmnn 16711 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 32 | 30, 31 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑃 ∈ ℕ) |
| 33 | 32 | nnred 12281 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑃 ∈ ℝ) |
| 34 | 32 | nnge1d 12314 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 1 ≤ 𝑃) |
| 35 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 36 | 35 | subg0cl 19152 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝑘) |
| 37 | 12, 36 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (0g‘𝐺) ∈ 𝑘) |
| 38 | 37 | ne0d 4342 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑘 ≠ ∅) |
| 39 | | hashnncl 14405 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ Fin →
((♯‘𝑘) ∈
ℕ ↔ 𝑘 ≠
∅)) |
| 40 | 15, 39 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → ((♯‘𝑘) ∈ ℕ ↔ 𝑘 ≠ ∅)) |
| 41 | 38, 40 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (♯‘𝑘) ∈ ℕ) |
| 42 | 30, 41 | pccld 16888 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (𝑃 pCnt (♯‘𝑘)) ∈
ℕ0) |
| 43 | 42 | nn0zd 12639 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (𝑃 pCnt (♯‘𝑘)) ∈ ℤ) |
| 44 | | simpl1 1192 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → 𝐺 ∈ Grp) |
| 45 | 4 | grpbn0 18984 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ Grp → 𝑋 ≠ ∅) |
| 46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → 𝑋 ≠ ∅) |
| 47 | | hashnncl 14405 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ Fin →
((♯‘𝑋) ∈
ℕ ↔ 𝑋 ≠
∅)) |
| 48 | 10, 47 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅)) |
| 49 | 46, 48 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → (♯‘𝑋) ∈
ℕ) |
| 50 | 8, 49 | pccld 16888 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → (𝑃 pCnt (♯‘𝑋)) ∈
ℕ0) |
| 51 | 50 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (𝑃 pCnt (♯‘𝑋)) ∈
ℕ0) |
| 52 | 51 | nn0zd 12639 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (𝑃 pCnt (♯‘𝑋)) ∈ ℤ) |
| 53 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑃 → (𝑝 pCnt (♯‘𝑘)) = (𝑃 pCnt (♯‘𝑘))) |
| 54 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑃 → (𝑝 pCnt (♯‘𝑋)) = (𝑃 pCnt (♯‘𝑋))) |
| 55 | 53, 54 | breq12d 5156 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑃 → ((𝑝 pCnt (♯‘𝑘)) ≤ (𝑝 pCnt (♯‘𝑋)) ↔ (𝑃 pCnt (♯‘𝑘)) ≤ (𝑃 pCnt (♯‘𝑋)))) |
| 56 | 4 | lagsubg 19213 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin) → (♯‘𝑘) ∥ (♯‘𝑋)) |
| 57 | 12, 11, 56 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (♯‘𝑘) ∥ (♯‘𝑋)) |
| 58 | 41 | nnzd 12640 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (♯‘𝑘) ∈ ℤ) |
| 59 | 49 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (♯‘𝑋) ∈ ℕ) |
| 60 | 59 | nnzd 12640 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (♯‘𝑋) ∈ ℤ) |
| 61 | | pc2dvds 16917 |
. . . . . . . . . . . . . . 15
⊢
(((♯‘𝑘)
∈ ℤ ∧ (♯‘𝑋) ∈ ℤ) →
((♯‘𝑘) ∥
(♯‘𝑋) ↔
∀𝑝 ∈ ℙ
(𝑝 pCnt
(♯‘𝑘)) ≤
(𝑝 pCnt
(♯‘𝑋)))) |
| 62 | 58, 60, 61 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → ((♯‘𝑘) ∥ (♯‘𝑋) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (♯‘𝑘)) ≤ (𝑝 pCnt (♯‘𝑋)))) |
| 63 | 57, 62 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → ∀𝑝 ∈ ℙ (𝑝 pCnt (♯‘𝑘)) ≤ (𝑝 pCnt (♯‘𝑋))) |
| 64 | 55, 63, 30 | rspcdva 3623 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (𝑃 pCnt (♯‘𝑘)) ≤ (𝑃 pCnt (♯‘𝑋))) |
| 65 | | eluz2 12884 |
. . . . . . . . . . . 12
⊢ ((𝑃 pCnt (♯‘𝑋)) ∈
(ℤ≥‘(𝑃 pCnt (♯‘𝑘))) ↔ ((𝑃 pCnt (♯‘𝑘)) ∈ ℤ ∧ (𝑃 pCnt (♯‘𝑋)) ∈ ℤ ∧ (𝑃 pCnt (♯‘𝑘)) ≤ (𝑃 pCnt (♯‘𝑋)))) |
| 66 | 43, 52, 64, 65 | syl3anbrc 1344 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (𝑃 pCnt (♯‘𝑋)) ∈
(ℤ≥‘(𝑃 pCnt (♯‘𝑘)))) |
| 67 | 33, 34, 66 | leexp2ad 14293 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (𝑃↑(𝑃 pCnt (♯‘𝑘))) ≤ (𝑃↑(𝑃 pCnt (♯‘𝑋)))) |
| 68 | 29 | simprd 495 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → ∃𝑛 ∈ ℕ0
(♯‘(Base‘(𝐺 ↾s 𝑘))) = (𝑃↑𝑛)) |
| 69 | 24 | fveqeq2d 6914 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → ((♯‘𝑘) = (𝑃↑𝑛) ↔ (♯‘(Base‘(𝐺 ↾s 𝑘))) = (𝑃↑𝑛))) |
| 70 | 69 | rexbidv 3179 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (∃𝑛 ∈ ℕ0
(♯‘𝑘) = (𝑃↑𝑛) ↔ ∃𝑛 ∈ ℕ0
(♯‘(Base‘(𝐺 ↾s 𝑘))) = (𝑃↑𝑛))) |
| 71 | 68, 70 | mpbird 257 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → ∃𝑛 ∈ ℕ0
(♯‘𝑘) = (𝑃↑𝑛)) |
| 72 | | pcprmpw 16921 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧
(♯‘𝑘) ∈
ℕ) → (∃𝑛
∈ ℕ0 (♯‘𝑘) = (𝑃↑𝑛) ↔ (♯‘𝑘) = (𝑃↑(𝑃 pCnt (♯‘𝑘))))) |
| 73 | 30, 41, 72 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (∃𝑛 ∈ ℕ0
(♯‘𝑘) = (𝑃↑𝑛) ↔ (♯‘𝑘) = (𝑃↑(𝑃 pCnt (♯‘𝑘))))) |
| 74 | 71, 73 | mpbid 232 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (♯‘𝑘) = (𝑃↑(𝑃 pCnt (♯‘𝑘)))) |
| 75 | | simplrr 778 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋)))) |
| 76 | 67, 74, 75 | 3brtr4d 5175 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → (♯‘𝑘) ≤ (♯‘𝐻)) |
| 77 | 4 | subgss 19145 |
. . . . . . . . . . . . 13
⊢ (𝐻 ∈ (SubGrp‘𝐺) → 𝐻 ⊆ 𝑋) |
| 78 | 77 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → 𝐻 ⊆ 𝑋) |
| 79 | 10, 78 | ssfid 9301 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → 𝐻 ∈ Fin) |
| 80 | 79 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝐻 ∈ Fin) |
| 81 | | hashdom 14418 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ Fin ∧ 𝐻 ∈ Fin) →
((♯‘𝑘) ≤
(♯‘𝐻) ↔
𝑘 ≼ 𝐻)) |
| 82 | 15, 80, 81 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → ((♯‘𝑘) ≤ (♯‘𝐻) ↔ 𝑘 ≼ 𝐻)) |
| 83 | 76, 82 | mpbid 232 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝑘 ≼ 𝐻) |
| 84 | | sbth 9133 |
. . . . . . . 8
⊢ ((𝐻 ≼ 𝑘 ∧ 𝑘 ≼ 𝐻) → 𝐻 ≈ 𝑘) |
| 85 | 18, 83, 84 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝐻 ≈ 𝑘) |
| 86 | | fisseneq 9293 |
. . . . . . 7
⊢ ((𝑘 ∈ Fin ∧ 𝐻 ⊆ 𝑘 ∧ 𝐻 ≈ 𝑘) → 𝐻 = 𝑘) |
| 87 | 15, 16, 85, 86 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ (𝑘 ∈ (SubGrp‘𝐺) ∧ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) → 𝐻 = 𝑘) |
| 88 | 87 | expr 456 |
. . . . 5
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ 𝑘 ∈ (SubGrp‘𝐺)) → ((𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)) → 𝐻 = 𝑘)) |
| 89 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝐺 ↾s 𝐻) = (𝐺 ↾s 𝐻) |
| 90 | 89 | subgbas 19148 |
. . . . . . . . . . . 12
⊢ (𝐻 ∈ (SubGrp‘𝐺) → 𝐻 = (Base‘(𝐺 ↾s 𝐻))) |
| 91 | 90 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → 𝐻 = (Base‘(𝐺 ↾s 𝐻))) |
| 92 | 91 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → (♯‘𝐻) =
(♯‘(Base‘(𝐺 ↾s 𝐻)))) |
| 93 | | simprr 773 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋)))) |
| 94 | 92, 93 | eqtr3d 2779 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) →
(♯‘(Base‘(𝐺 ↾s 𝐻))) = (𝑃↑(𝑃 pCnt (♯‘𝑋)))) |
| 95 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑃 pCnt (♯‘𝑋)) → (𝑃↑𝑛) = (𝑃↑(𝑃 pCnt (♯‘𝑋)))) |
| 96 | 95 | rspceeqv 3645 |
. . . . . . . . 9
⊢ (((𝑃 pCnt (♯‘𝑋)) ∈ ℕ0
∧ (♯‘(Base‘(𝐺 ↾s 𝐻))) = (𝑃↑(𝑃 pCnt (♯‘𝑋)))) → ∃𝑛 ∈ ℕ0
(♯‘(Base‘(𝐺 ↾s 𝐻))) = (𝑃↑𝑛)) |
| 97 | 50, 94, 96 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → ∃𝑛 ∈ ℕ0
(♯‘(Base‘(𝐺 ↾s 𝐻))) = (𝑃↑𝑛)) |
| 98 | 89 | subggrp 19147 |
. . . . . . . . . 10
⊢ (𝐻 ∈ (SubGrp‘𝐺) → (𝐺 ↾s 𝐻) ∈ Grp) |
| 99 | 98 | ad2antrl 728 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → (𝐺 ↾s 𝐻) ∈ Grp) |
| 100 | 91, 79 | eqeltrrd 2842 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → (Base‘(𝐺 ↾s 𝐻)) ∈ Fin) |
| 101 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘(𝐺
↾s 𝐻)) =
(Base‘(𝐺
↾s 𝐻)) |
| 102 | 101 | pgpfi 19623 |
. . . . . . . . 9
⊢ (((𝐺 ↾s 𝐻) ∈ Grp ∧
(Base‘(𝐺
↾s 𝐻))
∈ Fin) → (𝑃 pGrp
(𝐺 ↾s
𝐻) ↔ (𝑃 ∈ ℙ ∧
∃𝑛 ∈
ℕ0 (♯‘(Base‘(𝐺 ↾s 𝐻))) = (𝑃↑𝑛)))) |
| 103 | 99, 100, 102 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → (𝑃 pGrp (𝐺 ↾s 𝐻) ↔ (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0
(♯‘(Base‘(𝐺 ↾s 𝐻))) = (𝑃↑𝑛)))) |
| 104 | 8, 97, 103 | mpbir2and 713 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → 𝑃 pGrp (𝐺 ↾s 𝐻)) |
| 105 | 104 | adantr 480 |
. . . . . 6
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ 𝑘 ∈ (SubGrp‘𝐺)) → 𝑃 pGrp (𝐺 ↾s 𝐻)) |
| 106 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝐻 = 𝑘 → (𝐺 ↾s 𝐻) = (𝐺 ↾s 𝑘)) |
| 107 | 106 | breq2d 5155 |
. . . . . . 7
⊢ (𝐻 = 𝑘 → (𝑃 pGrp (𝐺 ↾s 𝐻) ↔ 𝑃 pGrp (𝐺 ↾s 𝑘))) |
| 108 | | eqimss 4042 |
. . . . . . . 8
⊢ (𝐻 = 𝑘 → 𝐻 ⊆ 𝑘) |
| 109 | 108 | biantrurd 532 |
. . . . . . 7
⊢ (𝐻 = 𝑘 → (𝑃 pGrp (𝐺 ↾s 𝑘) ↔ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) |
| 110 | 107, 109 | bitrd 279 |
. . . . . 6
⊢ (𝐻 = 𝑘 → (𝑃 pGrp (𝐺 ↾s 𝐻) ↔ (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) |
| 111 | 105, 110 | syl5ibcom 245 |
. . . . 5
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ 𝑘 ∈ (SubGrp‘𝐺)) → (𝐻 = 𝑘 → (𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)))) |
| 112 | 88, 111 | impbid 212 |
. . . 4
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) ∧ 𝑘 ∈ (SubGrp‘𝐺)) → ((𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)) ↔ 𝐻 = 𝑘)) |
| 113 | 112 | ralrimiva 3146 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → ∀𝑘 ∈ (SubGrp‘𝐺)((𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)) ↔ 𝐻 = 𝑘)) |
| 114 | | isslw 19626 |
. . 3
⊢ (𝐻 ∈ (𝑃 pSyl 𝐺) ↔ (𝑃 ∈ ℙ ∧ 𝐻 ∈ (SubGrp‘𝐺) ∧ ∀𝑘 ∈ (SubGrp‘𝐺)((𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)) ↔ 𝐻 = 𝑘))) |
| 115 | 8, 9, 113, 114 | syl3anbrc 1344 |
. 2
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) → 𝐻 ∈ (𝑃 pSyl 𝐺)) |
| 116 | 7, 115 | impbida 801 |
1
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) → (𝐻 ∈ (𝑃 pSyl 𝐺) ↔ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋)))))) |