Metamath Proof Explorer

Theorem slwpgp

Description: A Sylow P -subgroup is a P -group. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypothesis slwpgp.1 ⊢ S = G ↾ 𝑠 H
Assertion slwpgp ⊢ H ∈ P pSyl G → P pGrp S

Proof

Step Hyp Ref Expression
1 slwpgp.1 ⊢ S = G ↾ 𝑠 H
2 eqid ⊢ H = H
3 slwsubg ⊢ H ∈ P pSyl G → H ∈ SubGrp ⁡ G
4 1 slwispgp ⊢ H ∈ P pSyl G ∧ H ∈ SubGrp ⁡ G → H ⊆ H ∧ P pGrp S ↔ H = H
5 3 4 mpdan ⊢ H ∈ P pSyl G → H ⊆ H ∧ P pGrp S ↔ H = H
6 2 5 mpbiri ⊢ H ∈ P pSyl G → H ⊆ H ∧ P pGrp S
7 6 simprd ⊢ H ∈ P pSyl G → P pGrp S