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 \in (P pSyl G) \to P pGrp S$

Step	Hyp	Ref	Expression
1		slwpgp.1	$⊢ S = G ↾_{𝑠} H$
2		eqid	$⊢ H = H$
3		slwsubg	$⊢ H \in (P pSyl G) \to H \in SubGrp (G)$
4	1	slwispgp	$⊢ (H \in (P pSyl G) \land H \in SubGrp (G)) \to ((H \subseteq H \land P pGrp S) \leftrightarrow H = H)$
5	3 4	mpdan	$⊢ H \in (P pSyl G) \to ((H \subseteq H \land P pGrp S) \leftrightarrow H = H)$
6	2 5	mpbiri	$⊢ H \in (P pSyl G) \to (H \subseteq H \land P pGrp S)$
7	6	simprd	$⊢ H \in (P pSyl G) \to P pGrp S$

Metamath Proof Explorer