Theorem 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={\mathrm{Base}}_G$$
	sylow2b.xf	$$⊢\phi \to X\in \mathrm{Fin}$$
	sylow2b.h	$$⊢\phi \to H\in \mathrm{SubGrp}\left(G\right)$$
	sylow2b.k	$$⊢\phi \to K\in \mathrm{SubGrp}\left(G\right)$$
	sylow2b.a	$$⊢\underset{\dot{}}{+}={+}_G$$
	sylow2b.hp	$$⊢\phi \to P\mathrm{pGrp}\left(G{\upharpoonright }_{𝑠}H\right)$$
	sylow2b.kn	$$⊢\phi \to \left|K\right|=P^{P\mathrm{pCnt}\left|X\right|}$$
	sylow2b.d	$$⊢\underset{\dot{}}{-}={-}_G$$
Assertion	sylow2b	$$⊢\phi \to \exists g\in XH\subseteq \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)$$

Proof

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