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 𝐻 )
Assertion slwpgp ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) → 𝑃 pGrp 𝑆 )

Proof

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