isslw

Description: The property of being a Sylow subgroup. A Sylow P -subgroup is a P -group which has no proper supersets that are also P -groups. (Contributed by Mario Carneiro, 16-Jan-2015)

		Ref	Expression
	Assertion	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))$

Proof

Step	Hyp	Ref	Expression
1		df-slw	$⊢ pSyl = (p \in ℙ, g \in Grp ⟼ \{h \in SubGrp (g) \| \forall k \in SubGrp (g) ((h \subseteq k \land p pGrp (g ↾_{𝑠} k)) \leftrightarrow h = k)\})$
2	1	elmpocl	$⊢ H \in (P pSyl G) \to (P \in ℙ \land G \in Grp)$
3		simp1	$⊢ (P \in ℙ \land H \in SubGrp (G) \land \forall k \in SubGrp (G) ((H \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow H = k)) \to P \in ℙ$
4		subgrcl	$⊢ H \in SubGrp (G) \to G \in Grp$
5	4	3ad2ant2	$⊢ (P \in ℙ \land H \in SubGrp (G) \land \forall k \in SubGrp (G) ((H \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow H = k)) \to G \in Grp$
6	3 5	jca	$⊢ (P \in ℙ \land H \in SubGrp (G) \land \forall k \in SubGrp (G) ((H \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow H = k)) \to (P \in ℙ \land G \in Grp)$
7		simpr	$⊢ (p = P \land g = G) \to g = G$
8	7	fveq2d	$⊢ (p = P \land g = G) \to SubGrp (g) = SubGrp (G)$
9		simpl	$⊢ (p = P \land g = G) \to p = P$
10	7	oveq1d	$⊢ (p = P \land g = G) \to g ↾_{𝑠} k = G ↾_{𝑠} k$
11	9 10	breq12d	$⊢ (p = P \land g = G) \to (p pGrp (g ↾_{𝑠} k) \leftrightarrow P pGrp (G ↾_{𝑠} k))$
12	11	anbi2d	$⊢ (p = P \land g = G) \to ((h \subseteq k \land p pGrp (g ↾_{𝑠} k)) \leftrightarrow (h \subseteq k \land P pGrp (G ↾_{𝑠} k)))$
13	12	bibi1d	$⊢ (p = P \land g = G) \to (((h \subseteq k \land p pGrp (g ↾_{𝑠} k)) \leftrightarrow h = k) \leftrightarrow ((h \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow h = k))$
14	8 13	raleqbidv	$⊢ (p = P \land g = G) \to (\forall k \in SubGrp (g) ((h \subseteq k \land p pGrp (g ↾_{𝑠} k)) \leftrightarrow h = k) \leftrightarrow \forall k \in SubGrp (G) ((h \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow h = k))$
15	8 14	rabeqbidv	$⊢ (p = P \land g = G) \to \{h \in SubGrp (g) \| \forall k \in SubGrp (g) ((h \subseteq k \land p pGrp (g ↾_{𝑠} k)) \leftrightarrow h = k)\} = \{h \in SubGrp (G) \| \forall k \in SubGrp (G) ((h \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow h = k)\}$
16		fvex	$⊢ SubGrp (G) \in V$
17	16	rabex	$⊢ \{h \in SubGrp (G) \| \forall k \in SubGrp (G) ((h \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow h = k)\} \in V$
18	15 1 17	ovmpoa	$⊢ (P \in ℙ \land G \in Grp) \to P pSyl G = \{h \in SubGrp (G) \| \forall k \in SubGrp (G) ((h \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow h = k)\}$
19	18	eleq2d	$⊢ (P \in ℙ \land G \in Grp) \to (H \in (P pSyl G) \leftrightarrow H \in \{h \in SubGrp (G) \| \forall k \in SubGrp (G) ((h \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow h = k)\})$
20		cleq1lem	$⊢ h = H \to ((h \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow (H \subseteq k \land P pGrp (G ↾_{𝑠} k)))$
21		eqeq1	$⊢ h = H \to (h = k \leftrightarrow H = k)$
22	20 21	bibi12d	$⊢ h = H \to (((h \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow h = k) \leftrightarrow ((H \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow H = k))$
23	22	ralbidv	$⊢ h = H \to (\forall k \in SubGrp (G) ((h \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow h = k) \leftrightarrow \forall k \in SubGrp (G) ((H \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow H = k))$
24	23	elrab	$⊢ H \in \{h \in SubGrp (G) \| \forall k \in SubGrp (G) ((h \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow h = k)\} \leftrightarrow (H \in SubGrp (G) \land \forall k \in SubGrp (G) ((H \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow H = k))$
25	19 24	bitrdi	$⊢ (P \in ℙ \land G \in Grp) \to (H \in (P pSyl G) \leftrightarrow (H \in SubGrp (G) \land \forall k \in SubGrp (G) ((H \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow H = k)))$
26		simpl	$⊢ (P \in ℙ \land G \in Grp) \to P \in ℙ$
27	26	biantrurd	$⊢ (P \in ℙ \land G \in Grp) \to ((H \in SubGrp (G) \land \forall k \in SubGrp (G) ((H \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow H = k)) \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))))$
28	25 27	bitrd	$⊢ (P \in ℙ \land G \in Grp) \to (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))))$
29		3anass	$⊢ (P \in ℙ \land H \in SubGrp (G) \land \forall k \in SubGrp (G) ((H \subseteq k \land P pGrp (G ↾_{𝑠} k)) \leftrightarrow H = k)) \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)))$
30	28 29	bitr4di	$⊢ (P \in ℙ \land G \in Grp) \to (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)))$
31	2 6 30	pm5.21nii	$⊢ 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))$

Metamath Proof Explorer

Theorem isslw

Proof