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