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 |`s H )
Assertion slwpgp
|- ( H e. ( P pSyl G ) -> P pGrp S )

Proof

Step Hyp Ref Expression
1 slwpgp.1
 |-  S = ( G |`s H )
2 eqid
 |-  H = H
3 slwsubg
 |-  ( H e. ( P pSyl G ) -> H e. ( SubGrp ` G ) )
4 1 slwispgp
 |-  ( ( H e. ( P pSyl G ) /\ H e. ( SubGrp ` G ) ) -> ( ( H C_ H /\ P pGrp S ) <-> H = H ) )
5 3 4 mpdan
 |-  ( H e. ( P pSyl G ) -> ( ( H C_ H /\ P pGrp S ) <-> H = H ) )
6 2 5 mpbiri
 |-  ( H e. ( P pSyl G ) -> ( H C_ H /\ P pGrp S ) )
7 6 simprd
 |-  ( H e. ( P pSyl G ) -> P pGrp S )