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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	sylow2.f	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	sylow2.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) )
	sylow2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) )
	sylow2.a	⊢ + = ( +_g ‘ 𝐺 )
	sylow2.d	⊢ − = ( -_g ‘ 𝐺 )
Assertion	sylow2	⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝑋 𝐻 = ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sylow2.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		sylow2.f	⊢ ( 𝜑 → 𝑋 ∈ Fin )
3		sylow2.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) )
4		sylow2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) )
5		sylow2.a	⊢ + = ( +_g ‘ 𝐺 )
6		sylow2.d	⊢ − = ( -_g ‘ 𝐺 )
7	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ) ) → 𝑋 ∈ Fin )
8		slwsubg	⊢ ( 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
9	4 8	syl	⊢ ( 𝜑 → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
10		simprl	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ) ) → 𝑔 ∈ 𝑋 )
11		eqid	⊢ ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) = ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) )
12	1 5 6 11	conjsubg	⊢ ( ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑔 ∈ 𝑋 ) → ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ∈ ( SubGrp ‘ 𝐺 ) )
13	9 10 12	syl2an2r	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ) ) → ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ∈ ( SubGrp ‘ 𝐺 ) )
14	1	subgss	⊢ ( ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ∈ ( SubGrp ‘ 𝐺 ) → ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ⊆ 𝑋 )
15	13 14	syl	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ) ) → ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ⊆ 𝑋 )
16	7 15	ssfid	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ) ) → ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ∈ Fin )
17		simprr	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ) ) → 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) )
18	1 2 3	slwhash	⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) )
19	1 2 4	slwhash	⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) )
20	18 19	eqtr4d	⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) = ( ♯ ‘ 𝐾 ) )
21		slwsubg	⊢ ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
22	3 21	syl	⊢ ( 𝜑 → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
23	1	subgss	⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 ⊆ 𝑋 )
24	22 23	syl	⊢ ( 𝜑 → 𝐻 ⊆ 𝑋 )
25	2 24	ssfid	⊢ ( 𝜑 → 𝐻 ∈ Fin )
26	1	subgss	⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → 𝐾 ⊆ 𝑋 )
27	9 26	syl	⊢ ( 𝜑 → 𝐾 ⊆ 𝑋 )
28	2 27	ssfid	⊢ ( 𝜑 → 𝐾 ∈ Fin )
29		hashen	⊢ ( ( 𝐻 ∈ Fin ∧ 𝐾 ∈ Fin ) → ( ( ♯ ‘ 𝐻 ) = ( ♯ ‘ 𝐾 ) ↔ 𝐻 ≈ 𝐾 ) )
30	25 28 29	syl2anc	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) = ( ♯ ‘ 𝐾 ) ↔ 𝐻 ≈ 𝐾 ) )
31	20 30	mpbid	⊢ ( 𝜑 → 𝐻 ≈ 𝐾 )
32	1 5 6 11	conjsubgen	⊢ ( ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑔 ∈ 𝑋 ) → 𝐾 ≈ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) )
33	9 10 32	syl2an2r	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ) ) → 𝐾 ≈ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) )
34		entr	⊢ ( ( 𝐻 ≈ 𝐾 ∧ 𝐾 ≈ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ) → 𝐻 ≈ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) )
35	31 33 34	syl2an2r	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ) ) → 𝐻 ≈ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) )
36		fisseneq	⊢ ( ( ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ∈ Fin ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ∧ 𝐻 ≈ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ) → 𝐻 = ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) )
37	16 17 35 36	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ) ) → 𝐻 = ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) )
38		eqid	⊢ ( 𝐺 ↾_s 𝐻 ) = ( 𝐺 ↾_s 𝐻 )
39	38	slwpgp	⊢ ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) → 𝑃 pGrp ( 𝐺 ↾_s 𝐻 ) )
40	3 39	syl	⊢ ( 𝜑 → 𝑃 pGrp ( 𝐺 ↾_s 𝐻 ) )
41	1 2 22 9 5 40 19 6	sylow2b	⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝑋 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) )
42	37 41	reximddv	⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝑋 𝐻 = ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) )

Metamath Proof Explorer

Theorem sylow2

Proof