Theorem sylow2

Description: Sylow's second theorem. See also sylow2b for the "hard" part of the proof. Any two Sylow P -subgroups are conjugate to one another, and hence the same size, namely P ^ ( P pCnt | X | ) (see fislw ). This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 18-Jan-2015)

	Ref	Expression
Hypotheses	sylow2.x	$$⊢X={\mathrm{Base}}_G$$
	sylow2.f	$$⊢\phi \to X\in \mathrm{Fin}$$
	sylow2.h	$$⊢\phi \to H\in \left(P\mathrm{pSyl}G\right)$$
	sylow2.k	$$⊢\phi \to K\in \left(P\mathrm{pSyl}G\right)$$
	sylow2.a	$$⊢\underset{\dot{}}{+}={+}_G$$
	sylow2.d	$$⊢\underset{\dot{}}{-}={-}_G$$
Assertion	sylow2	$$⊢\phi \to \exists g\in XH=\mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)$$

Proof

Step	Hyp	Ref	Expression
1		sylow2.x	$$⊢X={\mathrm{Base}}_G$$
2		sylow2.f	$$⊢\phi \to X\in \mathrm{Fin}$$
3		sylow2.h	$$⊢\phi \to H\in \left(P\mathrm{pSyl}G\right)$$
4		sylow2.k	$$⊢\phi \to K\in \left(P\mathrm{pSyl}G\right)$$
5		sylow2.a	$$⊢\underset{\dot{}}{+}={+}_G$$
6		sylow2.d	$$⊢\underset{\dot{}}{-}={-}_G$$
7	2	adantr	$$⊢\left(\phi \wedge \left(g\in X\wedge H\subseteq \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)\right)\right)\to X\in \mathrm{Fin}$$
8		slwsubg	$$⊢K\in \left(P\mathrm{pSyl}G\right)\to K\in \mathrm{SubGrp}\left(G\right)$$
9	4 8	syl	$$⊢\phi \to K\in \mathrm{SubGrp}\left(G\right)$$
10		simprl	$$⊢\left(\phi \wedge \left(g\in X\wedge H\subseteq \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)\right)\right)\to g\in X$$
11		eqid	$$⊢\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)=\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)$$
12	1 5 6 11	conjsubg	$$⊢\left(K\in \mathrm{SubGrp}\left(G\right)\wedge g\in X\right)\to \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)\in \mathrm{SubGrp}\left(G\right)$$
13	9 10 12	syl2an2r	$$⊢\left(\phi \wedge \left(g\in X\wedge H\subseteq \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)\right)\right)\to \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)\in \mathrm{SubGrp}\left(G\right)$$
14	1	subgss	$$⊢\mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)\in \mathrm{SubGrp}\left(G\right)\to \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)\subseteq X$$
15	13 14	syl	$$⊢\left(\phi \wedge \left(g\in X\wedge H\subseteq \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)\right)\right)\to \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)\subseteq X$$
16	7 15	ssfid	$$⊢\left(\phi \wedge \left(g\in X\wedge H\subseteq \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)\right)\right)\to \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)\in \mathrm{Fin}$$
17		simprr	$$⊢\left(\phi \wedge \left(g\in X\wedge H\subseteq \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)\right)\right)\to H\subseteq \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)$$
18	1 2 3	slwhash	$$⊢\phi \to \left|H\right|=P^{P\mathrm{pCnt}\left|X\right|}$$
19	1 2 4	slwhash	$$⊢\phi \to \left|K\right|=P^{P\mathrm{pCnt}\left|X\right|}$$
20	18 19	eqtr4d	$$⊢\phi \to \left|H\right|=\left|K\right|$$
21		slwsubg	$$⊢H\in \left(P\mathrm{pSyl}G\right)\to H\in \mathrm{SubGrp}\left(G\right)$$
22	3 21	syl	$$⊢\phi \to H\in \mathrm{SubGrp}\left(G\right)$$
23	1	subgss	$$⊢H\in \mathrm{SubGrp}\left(G\right)\to H\subseteq X$$
24	22 23	syl	$$⊢\phi \to H\subseteq X$$
25	2 24	ssfid	$$⊢\phi \to H\in \mathrm{Fin}$$
26	1	subgss	$$⊢K\in \mathrm{SubGrp}\left(G\right)\to K\subseteq X$$
27	9 26	syl	$$⊢\phi \to K\subseteq X$$
28	2 27	ssfid	$$⊢\phi \to K\in \mathrm{Fin}$$
29		hashen	$$⊢\left(H\in \mathrm{Fin}\wedge K\in \mathrm{Fin}\right)\to \left(\left|H\right|=\left|K\right|\leftrightarrow H\approx K\right)$$
30	25 28 29	syl2anc	$$⊢\phi \to \left(\left|H\right|=\left|K\right|\leftrightarrow H\approx K\right)$$
31	20 30	mpbid	$$⊢\phi \to H\approx K$$
32	1 5 6 11	conjsubgen	$$⊢\left(K\in \mathrm{SubGrp}\left(G\right)\wedge g\in X\right)\to K\approx \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)$$
33	9 10 32	syl2an2r	$$⊢\left(\phi \wedge \left(g\in X\wedge H\subseteq \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)\right)\right)\to K\approx \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)$$
34		entr	$$⊢\left(H\approx K\wedge K\approx \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)\right)\to H\approx \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)$$
35	31 33 34	syl2an2r	$$⊢\left(\phi \wedge \left(g\in X\wedge H\subseteq \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)\right)\right)\to H\approx \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)$$
36		fisseneq	$$⊢\left(\mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)\in \mathrm{Fin}\wedge H\subseteq \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)\wedge H\approx \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)\right)\to H=\mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)$$
37	16 17 35 36	syl3anc	$$⊢\left(\phi \wedge \left(g\in X\wedge H\subseteq \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)\right)\right)\to H=\mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)$$
38		eqid	$$⊢G{\upharpoonright }_{𝑠}H=G{\upharpoonright }_{𝑠}H$$
39	38	slwpgp	$$⊢H\in \left(P\mathrm{pSyl}G\right)\to P\mathrm{pGrp}\left(G{\upharpoonright }_{𝑠}H\right)$$
40	3 39	syl	$$⊢\phi \to P\mathrm{pGrp}\left(G{\upharpoonright }_{𝑠}H\right)$$
41	1 2 22 9 5 40 19 6	sylow2b	$$⊢\phi \to \exists g\in XH\subseteq \mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)$$
42	37 41	reximddv	$$⊢\phi \to \exists g\in XH=\mathrm{ran}\left(x\in K⟼\left(g\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}g\right)$$