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 ) |
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 ) |