Theorem sylow3lem4

Description: Lemma for sylow3 , first part. The number of Sylow subgroups is a divisor of the size of G reduced by the size of a Sylow subgroup of G . (Contributed by Mario Carneiro, 19-Jan-2015)

	Ref	Expression
Hypotheses	sylow3.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	sylow3.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	sylow3.xf	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	sylow3.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	sylow3lem1.a	⊢ + = ( +g ‘ 𝐺 )
	sylow3lem1.d	⊢ − = ( -g ‘ 𝐺 )
	sylow3lem1.m	⊢ ⊕ = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) )
	sylow3lem2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) )
	sylow3lem2.h	⊢ 𝐻 = { 𝑢 ∈ 𝑋 ∣ ( 𝑢 ⊕ 𝐾 ) = 𝐾 }
	sylow3lem2.n	⊢ 𝑁 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝐾 ↔ ( 𝑦 + 𝑥 ) ∈ 𝐾 ) }
Assertion	sylow3lem4	⊢ ( 𝜑 → ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) ∥ ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		sylow3.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		sylow3.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
3		sylow3.xf	⊢ ( 𝜑 → 𝑋 ∈ Fin )
4		sylow3.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5		sylow3lem1.a	⊢ + = ( +g ‘ 𝐺 )
6		sylow3lem1.d	⊢ − = ( -g ‘ 𝐺 )
7		sylow3lem1.m	⊢ ⊕ = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) )
8		sylow3lem2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) )
9		sylow3lem2.h	⊢ 𝐻 = { 𝑢 ∈ 𝑋 ∣ ( 𝑢 ⊕ 𝐾 ) = 𝐾 }
10		sylow3lem2.n	⊢ 𝑁 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝐾 ↔ ( 𝑦 + 𝑥 ) ∈ 𝐾 ) }
11	1 2 3 4 5 6 7 8 9 10	sylow3lem3	⊢ ( 𝜑 → ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) = ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) )
12		slwsubg	⊢ ( 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
13	8 12	syl	⊢ ( 𝜑 → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
14		eqid	⊢ ( 𝐺 ↾s 𝑁 ) = ( 𝐺 ↾s 𝑁 )
15	10 1 5 14	nmznsg	⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → 𝐾 ∈ ( NrmSGrp ‘ ( 𝐺 ↾s 𝑁 ) ) )
16		nsgsubg	⊢ ( 𝐾 ∈ ( NrmSGrp ‘ ( 𝐺 ↾s 𝑁 ) ) → 𝐾 ∈ ( SubGrp ‘ ( 𝐺 ↾s 𝑁 ) ) )
17	15 16	syl	⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → 𝐾 ∈ ( SubGrp ‘ ( 𝐺 ↾s 𝑁 ) ) )
18	13 17	syl	⊢ ( 𝜑 → 𝐾 ∈ ( SubGrp ‘ ( 𝐺 ↾s 𝑁 ) ) )
19	10 1 5	nmzsubg	⊢ ( 𝐺 ∈ Grp → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
20	2 19	syl	⊢ ( 𝜑 → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
21	14	subgbas	⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → 𝑁 = ( Base ‘ ( 𝐺 ↾s 𝑁 ) ) )
22	20 21	syl	⊢ ( 𝜑 → 𝑁 = ( Base ‘ ( 𝐺 ↾s 𝑁 ) ) )
23	1	subgss	⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → 𝑁 ⊆ 𝑋 )
24	20 23	syl	⊢ ( 𝜑 → 𝑁 ⊆ 𝑋 )
25	3 24	ssfid	⊢ ( 𝜑 → 𝑁 ∈ Fin )
26	22 25	eqeltrrd	⊢ ( 𝜑 → ( Base ‘ ( 𝐺 ↾s 𝑁 ) ) ∈ Fin )
27		eqid	⊢ ( Base ‘ ( 𝐺 ↾s 𝑁 ) ) = ( Base ‘ ( 𝐺 ↾s 𝑁 ) )
28	27	lagsubg	⊢ ( ( 𝐾 ∈ ( SubGrp ‘ ( 𝐺 ↾s 𝑁 ) ) ∧ ( Base ‘ ( 𝐺 ↾s 𝑁 ) ) ∈ Fin ) → ( ♯ ‘ 𝐾 ) ∥ ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝑁 ) ) ) )
29	18 26 28	syl2anc	⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ∥ ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝑁 ) ) ) )
30	22	fveq2d	⊢ ( 𝜑 → ( ♯ ‘ 𝑁 ) = ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝑁 ) ) ) )
31	29 30	breqtrrd	⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ∥ ( ♯ ‘ 𝑁 ) )
32		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
33	32	subg0cl	⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝐾 )
34	13 33	syl	⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ 𝐾 )
35	34	ne0d	⊢ ( 𝜑 → 𝐾 ≠ ∅ )
36	1	subgss	⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → 𝐾 ⊆ 𝑋 )
37	13 36	syl	⊢ ( 𝜑 → 𝐾 ⊆ 𝑋 )
38	3 37	ssfid	⊢ ( 𝜑 → 𝐾 ∈ Fin )
39		hashnncl	⊢ ( 𝐾 ∈ Fin → ( ( ♯ ‘ 𝐾 ) ∈ ℕ ↔ 𝐾 ≠ ∅ ) )
40	38 39	syl	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐾 ) ∈ ℕ ↔ 𝐾 ≠ ∅ ) )
41	35 40	mpbird	⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ∈ ℕ )
42	41	nnzd	⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ∈ ℤ )
43		hashcl	⊢ ( 𝑁 ∈ Fin → ( ♯ ‘ 𝑁 ) ∈ ℕ0 )
44	25 43	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝑁 ) ∈ ℕ0 )
45	44	nn0zd	⊢ ( 𝜑 → ( ♯ ‘ 𝑁 ) ∈ ℤ )
46		pwfi	⊢ ( 𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin )
47	3 46	sylib	⊢ ( 𝜑 → 𝒫 𝑋 ∈ Fin )
48		eqid	⊢ ( 𝐺 ~QG 𝑁 ) = ( 𝐺 ~QG 𝑁 )
49	1 48	eqger	⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ~QG 𝑁 ) Er 𝑋 )
50	20 49	syl	⊢ ( 𝜑 → ( 𝐺 ~QG 𝑁 ) Er 𝑋 )
51	50	qsss	⊢ ( 𝜑 → ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ⊆ 𝒫 𝑋 )
52	47 51	ssfid	⊢ ( 𝜑 → ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ∈ Fin )
53		hashcl	⊢ ( ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ∈ Fin → ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) ∈ ℕ0 )
54	52 53	syl	⊢ ( 𝜑 → ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) ∈ ℕ0 )
55	54	nn0zd	⊢ ( 𝜑 → ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) ∈ ℤ )
56		dvdscmul	⊢ ( ( ( ♯ ‘ 𝐾 ) ∈ ℤ ∧ ( ♯ ‘ 𝑁 ) ∈ ℤ ∧ ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) ∈ ℤ ) → ( ( ♯ ‘ 𝐾 ) ∥ ( ♯ ‘ 𝑁 ) → ( ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) · ( ♯ ‘ 𝐾 ) ) ∥ ( ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) · ( ♯ ‘ 𝑁 ) ) ) )
57	42 45 55 56	syl3anc	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐾 ) ∥ ( ♯ ‘ 𝑁 ) → ( ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) · ( ♯ ‘ 𝐾 ) ) ∥ ( ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) · ( ♯ ‘ 𝑁 ) ) ) )
58	31 57	mpd	⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) · ( ♯ ‘ 𝐾 ) ) ∥ ( ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) · ( ♯ ‘ 𝑁 ) ) )
59		hashcl	⊢ ( 𝑋 ∈ Fin → ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
60	3 59	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
61	60	nn0cnd	⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℂ )
62	41	nncnd	⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ∈ ℂ )
63	41	nnne0d	⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ≠ 0 )
64	61 62 63	divcan1d	⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑋 ) / ( ♯ ‘ 𝐾 ) ) · ( ♯ ‘ 𝐾 ) ) = ( ♯ ‘ 𝑋 ) )
65	1 48 20 3	lagsubg2	⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) = ( ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) · ( ♯ ‘ 𝑁 ) ) )
66	64 65	eqtrd	⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑋 ) / ( ♯ ‘ 𝐾 ) ) · ( ♯ ‘ 𝐾 ) ) = ( ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) · ( ♯ ‘ 𝑁 ) ) )
67	58 66	breqtrrd	⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) · ( ♯ ‘ 𝐾 ) ) ∥ ( ( ( ♯ ‘ 𝑋 ) / ( ♯ ‘ 𝐾 ) ) · ( ♯ ‘ 𝐾 ) ) )
68	1	lagsubg	⊢ ( ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ 𝐾 ) ∥ ( ♯ ‘ 𝑋 ) )
69	13 3 68	syl2anc	⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ∥ ( ♯ ‘ 𝑋 ) )
70	60	nn0zd	⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℤ )
71		dvdsval2	⊢ ( ( ( ♯ ‘ 𝐾 ) ∈ ℤ ∧ ( ♯ ‘ 𝐾 ) ≠ 0 ∧ ( ♯ ‘ 𝑋 ) ∈ ℤ ) → ( ( ♯ ‘ 𝐾 ) ∥ ( ♯ ‘ 𝑋 ) ↔ ( ( ♯ ‘ 𝑋 ) / ( ♯ ‘ 𝐾 ) ) ∈ ℤ ) )
72	42 63 70 71	syl3anc	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐾 ) ∥ ( ♯ ‘ 𝑋 ) ↔ ( ( ♯ ‘ 𝑋 ) / ( ♯ ‘ 𝐾 ) ) ∈ ℤ ) )
73	69 72	mpbid	⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) / ( ♯ ‘ 𝐾 ) ) ∈ ℤ )
74		dvdsmulcr	⊢ ( ( ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) ∈ ℤ ∧ ( ( ♯ ‘ 𝑋 ) / ( ♯ ‘ 𝐾 ) ) ∈ ℤ ∧ ( ( ♯ ‘ 𝐾 ) ∈ ℤ ∧ ( ♯ ‘ 𝐾 ) ≠ 0 ) ) → ( ( ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) · ( ♯ ‘ 𝐾 ) ) ∥ ( ( ( ♯ ‘ 𝑋 ) / ( ♯ ‘ 𝐾 ) ) · ( ♯ ‘ 𝐾 ) ) ↔ ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) ∥ ( ( ♯ ‘ 𝑋 ) / ( ♯ ‘ 𝐾 ) ) ) )
75	55 73 42 63 74	syl112anc	⊢ ( 𝜑 → ( ( ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) · ( ♯ ‘ 𝐾 ) ) ∥ ( ( ( ♯ ‘ 𝑋 ) / ( ♯ ‘ 𝐾 ) ) · ( ♯ ‘ 𝐾 ) ) ↔ ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) ∥ ( ( ♯ ‘ 𝑋 ) / ( ♯ ‘ 𝐾 ) ) ) )
76	67 75	mpbid	⊢ ( 𝜑 → ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) ∥ ( ( ♯ ‘ 𝑋 ) / ( ♯ ‘ 𝐾 ) ) )
77	1 3 8	slwhash	⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) )
78	77	oveq2d	⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) / ( ♯ ‘ 𝐾 ) ) = ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )
79	76 78	breqtrd	⊢ ( 𝜑 → ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) ∥ ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )
80	11 79	eqbrtrd	⊢ ( 𝜑 → ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) ∥ ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )