Description: A Sylow P -subgroup is a P -group. (Contributed by Mario Carneiro, 16-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | slwpgp.1 | ⊢ 𝑆 = ( 𝐺 ↾s 𝐻 ) | |
Assertion | slwpgp | ⊢ ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) → 𝑃 pGrp 𝑆 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | slwpgp.1 | ⊢ 𝑆 = ( 𝐺 ↾s 𝐻 ) | |
2 | eqid | ⊢ 𝐻 = 𝐻 | |
3 | slwsubg | ⊢ ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) | |
4 | 1 | slwispgp | ⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝐻 ⊆ 𝐻 ∧ 𝑃 pGrp 𝑆 ) ↔ 𝐻 = 𝐻 ) ) |
5 | 3 4 | mpdan | ⊢ ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) → ( ( 𝐻 ⊆ 𝐻 ∧ 𝑃 pGrp 𝑆 ) ↔ 𝐻 = 𝐻 ) ) |
6 | 2 5 | mpbiri | ⊢ ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) → ( 𝐻 ⊆ 𝐻 ∧ 𝑃 pGrp 𝑆 ) ) |
7 | 6 | simprd | ⊢ ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) → 𝑃 pGrp 𝑆 ) |