sylow2b

Description: Sylow's second theorem. Any P -group H is a subgroup of a conjugated P -group K of order P ^ n || ( #X ) with n maximal. This is usually stated under the assumption that K is a Sylow subgroup, but we use a slightly different definition, whose equivalence to this one requires this theorem. This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 18-Jan-2015)

	Ref	Expression
Hypotheses	sylow2b.x	$⊢ X = {Base}_{G}$
	sylow2b.xf	$⊢ φ \to X \in Fin$
	sylow2b.h	$⊢ φ \to H \in SubGrp (G)$
	sylow2b.k	$⊢ φ \to K \in SubGrp (G)$
	sylow2b.a	$⊢ \underset{˙}{+} = +_{G}$
	sylow2b.hp	$⊢ φ \to P pGrp (G ↾_{𝑠} H)$
	sylow2b.kn	$⊢ φ \to \|K\| = P^{P pCnt \|X\|}$
	sylow2b.d	$⊢ \underset{˙}{-} = -_{G}$
Assertion	sylow2b	$⊢ φ \to \exists g \in X H \subseteq ran (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g)$

Proof

Step	Hyp	Ref	Expression
1		sylow2b.x	$⊢ X = {Base}_{G}$
2		sylow2b.xf	$⊢ φ \to X \in Fin$
3		sylow2b.h	$⊢ φ \to H \in SubGrp (G)$
4		sylow2b.k	$⊢ φ \to K \in SubGrp (G)$
5		sylow2b.a	$⊢ \underset{˙}{+} = +_{G}$
6		sylow2b.hp	$⊢ φ \to P pGrp (G ↾_{𝑠} H)$
7		sylow2b.kn	$⊢ φ \to \|K\| = P^{P pCnt \|X\|}$
8		sylow2b.d	$⊢ \underset{˙}{-} = -_{G}$
9		eqid	$⊢ G ~_{QG} K = G ~_{QG} K$
10		oveq2	$⊢ s = z \to u \underset{˙}{+} s = u \underset{˙}{+} z$
11	10	cbvmptv	$⊢ (s \in v ⟼ u \underset{˙}{+} s) = (z \in v ⟼ u \underset{˙}{+} z)$
12		oveq1	$⊢ u = x \to u \underset{˙}{+} z = x \underset{˙}{+} z$
13	12	mpteq2dv	$⊢ u = x \to (z \in v ⟼ u \underset{˙}{+} z) = (z \in v ⟼ x \underset{˙}{+} z)$
14	11 13	eqtrid	$⊢ u = x \to (s \in v ⟼ u \underset{˙}{+} s) = (z \in v ⟼ x \underset{˙}{+} z)$
15	14	rneqd	$⊢ u = x \to ran (s \in v ⟼ u \underset{˙}{+} s) = ran (z \in v ⟼ x \underset{˙}{+} z)$
16		mpteq1	$⊢ v = y \to (z \in v ⟼ x \underset{˙}{+} z) = (z \in y ⟼ x \underset{˙}{+} z)$
17	16	rneqd	$⊢ v = y \to ran (z \in v ⟼ x \underset{˙}{+} z) = ran (z \in y ⟼ x \underset{˙}{+} z)$
18	15 17	cbvmpov	$⊢ (u \in H, v \in (X / (G ~_{QG} K)) ⟼ ran (s \in v ⟼ u \underset{˙}{+} s)) = (x \in H, y \in (X / (G ~_{QG} K)) ⟼ ran (z \in y ⟼ x \underset{˙}{+} z))$
19	1 2 3 4 5 9 18 6 7 8	sylow2blem3	$⊢ φ \to \exists g \in X H \subseteq ran (x \in K ⟼ (g \underset{˙}{+} x) \underset{˙}{-} g)$

Metamath Proof Explorer

Theorem sylow2b

Proof