slwispgp

Description: Defining property of a Sylow P -subgroup. (Contributed by Mario Carneiro, 16-Jan-2015)

		Ref	Expression
	Hypothesis	slwispgp.1	$⊢ S = G ↾_{𝑠} K$
	Assertion	slwispgp	$⊢ (H \in (P pSyl G) \land K \in SubGrp (G)) \to ((H \subseteq K \land P pGrp S) \leftrightarrow H = K)$

Step	Hyp	Ref	Expression
1		slwispgp.1	$⊢ S = G ↾_{𝑠} K$
2		isslw	$⊢ H \in (P pSyl G) \leftrightarrow (P \in ℙ \land H \in SubGrp (G) \land \forall k \in SubGrp (G) ((H \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow H = k))$
3	2	simp3bi	$⊢ H \in (P pSyl G) \to \forall k \in SubGrp (G) ((H \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow H = k)$
4		sseq2	$⊢ k = K \to (H \subseteq k \leftrightarrow H \subseteq K)$
5		oveq2	$⊢ k = K \to G ↾_{𝑠} k = G ↾_{𝑠} K$
6	5 1	eqtr4di	$⊢ k = K \to G ↾_{𝑠} k = S$
7	6	breq2d	$⊢ k = K \to (P pGrp (G ↾_{𝑠} k) \leftrightarrow P pGrp S)$
8	4 7	anbi12d	$⊢ k = K \to ((H \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow (H \subseteq K \land P pGrp S))$
9		eqeq2	$⊢ k = K \to (H = k \leftrightarrow H = K)$
10	8 9	bibi12d	$⊢ k = K \to (((H \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow H = k) \leftrightarrow ((H \subseteq K \land P pGrp S) \leftrightarrow H = K))$
11	10	rspccva	$⊢ (\forall k \in SubGrp (G) ((H \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow H = k) \land K \in SubGrp (G)) \to ((H \subseteq K \land P pGrp S) \leftrightarrow H = K)$
12	3 11	sylan	$⊢ (H \in (P pSyl G) \land K \in SubGrp (G)) \to ((H \subseteq K \land P pGrp S) \leftrightarrow H = K)$

Metamath Proof Explorer