subgslw

Description: A Sylow subgroup that is contained in a larger subgroup is also Sylow with respect to the subgroup. (The converse need not be true.) (Contributed by Mario Carneiro, 19-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		subgslw.1	$⊢ H = G ↾_{𝑠} S$
2		slwprm	$⊢ K \in (P pSyl G) \to P \in ℙ$
3	2	3ad2ant2	$⊢ (S \in SubGrp (G) \land K \in (P pSyl G) \land K \subseteq S) \to P \in ℙ$
4		slwsubg	$⊢ K \in (P pSyl G) \to K \in SubGrp (G)$
5	4	3ad2ant2	$⊢ (S \in SubGrp (G) \land K \in (P pSyl G) \land K \subseteq S) \to K \in SubGrp (G)$
6		simp3	$⊢ (S \in SubGrp (G) \land K \in (P pSyl G) \land K \subseteq S) \to K \subseteq S$
7	1	subsubg	$⊢ S \in SubGrp (G) \to (K \in SubGrp (H) \leftrightarrow (K \in SubGrp (G) \land K \subseteq S))$
8	7	3ad2ant1	$⊢ (S \in SubGrp (G) \land K \in (P pSyl G) \land K \subseteq S) \to (K \in SubGrp (H) \leftrightarrow (K \in SubGrp (G) \land K \subseteq S))$
9	5 6 8	mpbir2and	$⊢ (S \in SubGrp (G) \land K \in (P pSyl G) \land K \subseteq S) \to K \in SubGrp (H)$
10	1	oveq1i	$⊢ H ↾_{𝑠} x = (G ↾_{𝑠} S) ↾_{𝑠} x$
11		simpl1	$⊢ ((S \in SubGrp (G) \land K \in (P pSyl G) \land K \subseteq S) \land x \in SubGrp (H)) \to S \in SubGrp (G)$
12	1	subsubg	$⊢ S \in SubGrp (G) \to (x \in SubGrp (H) \leftrightarrow (x \in SubGrp (G) \land x \subseteq S))$
13	12	3ad2ant1	$⊢ (S \in SubGrp (G) \land K \in (P pSyl G) \land K \subseteq S) \to (x \in SubGrp (H) \leftrightarrow (x \in SubGrp (G) \land x \subseteq S))$
14	13	simplbda	$⊢ ((S \in SubGrp (G) \land K \in (P pSyl G) \land K \subseteq S) \land x \in SubGrp (H)) \to x \subseteq S$
15		ressabs	$⊢ (S \in SubGrp (G) \land x \subseteq S) \to (G ↾_{𝑠} S) ↾_{𝑠} x = G ↾_{𝑠} x$
16	11 14 15	syl2anc	$⊢ ((S \in SubGrp (G) \land K \in (P pSyl G) \land K \subseteq S) \land x \in SubGrp (H)) \to (G ↾_{𝑠} S) ↾_{𝑠} x = G ↾_{𝑠} x$
17	10 16	syl5eq	$⊢ ((S \in SubGrp (G) \land K \in (P pSyl G) \land K \subseteq S) \land x \in SubGrp (H)) \to H ↾_{𝑠} x = G ↾_{𝑠} x$
18	17	breq2d	$⊢ ((S \in SubGrp (G) \land K \in (P pSyl G) \land K \subseteq S) \land x \in SubGrp (H)) \to (P pGrp (H ↾_{𝑠} x) \leftrightarrow P pGrp (G ↾_{𝑠} x))$
19	18	anbi2d	$⊢ ((S \in SubGrp (G) \land K \in (P pSyl G) \land K \subseteq S) \land x \in SubGrp (H)) \to ((K \subseteq x \land P pGrp (H ↾_{𝑠} x)) \leftrightarrow (K \subseteq x \land P pGrp (G ↾_{𝑠} x)))$
20		simpl2	$⊢ ((S \in SubGrp (G) \land K \in (P pSyl G) \land K \subseteq S) \land x \in SubGrp (H)) \to K \in (P pSyl G)$
21	13	simprbda	$⊢ ((S \in SubGrp (G) \land K \in (P pSyl G) \land K \subseteq S) \land x \in SubGrp (H)) \to x \in SubGrp (G)$
22		eqid	$⊢ G ↾_{𝑠} x = G ↾_{𝑠} x$
23	22	slwispgp	$⊢ (K \in (P pSyl G) \land x \in SubGrp (G)) \to ((K \subseteq x \land P pGrp (G ↾_{𝑠} x)) \leftrightarrow K = x)$
24	20 21 23	syl2anc	$⊢ ((S \in SubGrp (G) \land K \in (P pSyl G) \land K \subseteq S) \land x \in SubGrp (H)) \to ((K \subseteq x \land P pGrp (G ↾_{𝑠} x)) \leftrightarrow K = x)$
25	19 24	bitrd	$⊢ ((S \in SubGrp (G) \land K \in (P pSyl G) \land K \subseteq S) \land x \in SubGrp (H)) \to ((K \subseteq x \land P pGrp (H ↾_{𝑠} x)) \leftrightarrow K = x)$
26	25	ralrimiva	$⊢ (S \in SubGrp (G) \land K \in (P pSyl G) \land K \subseteq S) \to \forall x \in SubGrp (H) ((K \subseteq x \land P pGrp (H ↾_{𝑠} x)) \leftrightarrow K = x)$
27		isslw	$⊢ K \in (P pSyl H) \leftrightarrow (P \in ℙ \land K \in SubGrp (H) \land \forall x \in SubGrp (H) ((K \subseteq x \land P pGrp (H ↾_{𝑠} x)) \leftrightarrow K = x))$
28	3 9 26 27	syl3anbrc	$⊢ (S \in SubGrp (G) \land K \in (P pSyl G) \land K \subseteq S) \to K \in (P pSyl H)$

Metamath Proof Explorer

Theorem subgslw

Proof