sylow3lem6

Description: Lemma for sylow3 , second part. Using the lemma sylow2a , show that the number of sylow subgroups is equivalent mod P to the number of fixed points under the group action. But K is the unique element of the set of Sylow subgroups that is fixed under the group action, so there is exactly one fixed point and so ( ( #( P pSyl G ) ) mod P ) = 1 . (Contributed by Mario Carneiro, 19-Jan-2015)

	Ref	Expression
Hypotheses	sylow3.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	sylow3.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	sylow3.xf	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	sylow3.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	sylow3lem5.a	⊢ + = ( +_g ‘ 𝐺 )
	sylow3lem5.d	⊢ − = ( -_g ‘ 𝐺 )
	sylow3lem5.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) )
	sylow3lem5.m	⊢ ⊕ = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) )
	sylow3lem6.n	⊢ 𝑁 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑠 ) }
Assertion	sylow3lem6	⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) mod 𝑃 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		sylow3.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		sylow3.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
3		sylow3.xf	⊢ ( 𝜑 → 𝑋 ∈ Fin )
4		sylow3.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5		sylow3lem5.a	⊢ + = ( +_g ‘ 𝐺 )
6		sylow3lem5.d	⊢ − = ( -_g ‘ 𝐺 )
7		sylow3lem5.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) )
8		sylow3lem5.m	⊢ ⊕ = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) )
9		sylow3lem6.n	⊢ 𝑁 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑠 ) }
10		eqid	⊢ ( Base ‘ ( 𝐺 ↾_s 𝐾 ) ) = ( Base ‘ ( 𝐺 ↾_s 𝐾 ) )
11	1 2 3 4 5 6 7 8	sylow3lem5	⊢ ( 𝜑 → ⊕ ∈ ( ( 𝐺 ↾_s 𝐾 ) GrpAct ( 𝑃 pSyl 𝐺 ) ) )
12		eqid	⊢ ( 𝐺 ↾_s 𝐾 ) = ( 𝐺 ↾_s 𝐾 )
13	12	slwpgp	⊢ ( 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) → 𝑃 pGrp ( 𝐺 ↾_s 𝐾 ) )
14	7 13	syl	⊢ ( 𝜑 → 𝑃 pGrp ( 𝐺 ↾_s 𝐾 ) )
15		slwsubg	⊢ ( 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
16	7 15	syl	⊢ ( 𝜑 → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
17	12	subgbas	⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → 𝐾 = ( Base ‘ ( 𝐺 ↾_s 𝐾 ) ) )
18	16 17	syl	⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( 𝐺 ↾_s 𝐾 ) ) )
19	1	subgss	⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → 𝐾 ⊆ 𝑋 )
20	16 19	syl	⊢ ( 𝜑 → 𝐾 ⊆ 𝑋 )
21	3 20	ssfid	⊢ ( 𝜑 → 𝐾 ∈ Fin )
22	18 21	eqeltrrd	⊢ ( 𝜑 → ( Base ‘ ( 𝐺 ↾_s 𝐾 ) ) ∈ Fin )
23		pwfi	⊢ ( 𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin )
24	3 23	sylib	⊢ ( 𝜑 → 𝒫 𝑋 ∈ Fin )
25		slwsubg	⊢ ( 𝑥 ∈ ( 𝑃 pSyl 𝐺 ) → 𝑥 ∈ ( SubGrp ‘ 𝐺 ) )
26	1	subgss	⊢ ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) → 𝑥 ⊆ 𝑋 )
27	25 26	syl	⊢ ( 𝑥 ∈ ( 𝑃 pSyl 𝐺 ) → 𝑥 ⊆ 𝑋 )
28	25 27	elpwd	⊢ ( 𝑥 ∈ ( 𝑃 pSyl 𝐺 ) → 𝑥 ∈ 𝒫 𝑋 )
29	28	ssriv	⊢ ( 𝑃 pSyl 𝐺 ) ⊆ 𝒫 𝑋
30		ssfi	⊢ ( ( 𝒫 𝑋 ∈ Fin ∧ ( 𝑃 pSyl 𝐺 ) ⊆ 𝒫 𝑋 ) → ( 𝑃 pSyl 𝐺 ) ∈ Fin )
31	24 29 30	sylancl	⊢ ( 𝜑 → ( 𝑃 pSyl 𝐺 ) ∈ Fin )
32		eqid	⊢ { 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ∣ ∀ 𝑔 ∈ ( Base ‘ ( 𝐺 ↾_s 𝐾 ) ) ( 𝑔 ⊕ 𝑠 ) = 𝑠 } = { 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ∣ ∀ 𝑔 ∈ ( Base ‘ ( 𝐺 ↾_s 𝐾 ) ) ( 𝑔 ⊕ 𝑠 ) = 𝑠 }
33		eqid	⊢ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( { 𝑧 , 𝑤 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ ℎ ∈ ( Base ‘ ( 𝐺 ↾_s 𝐾 ) ) ( ℎ ⊕ 𝑧 ) = 𝑤 ) } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( { 𝑧 , 𝑤 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ ℎ ∈ ( Base ‘ ( 𝐺 ↾_s 𝐾 ) ) ( ℎ ⊕ 𝑧 ) = 𝑤 ) }
34	10 11 14 22 31 32 33	sylow2a	⊢ ( 𝜑 → 𝑃 ∥ ( ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) − ( ♯ ‘ { 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ∣ ∀ 𝑔 ∈ ( Base ‘ ( 𝐺 ↾_s 𝐾 ) ) ( 𝑔 ⊕ 𝑠 ) = 𝑠 } ) ) )
35		eqcom	⊢ ( ran ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) − 𝑔 ) ) = 𝑠 ↔ 𝑠 = ran ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) − 𝑔 ) ) )
36	20	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) → 𝐾 ⊆ 𝑋 )
37	36	sselda	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑔 ∈ 𝐾 ) → 𝑔 ∈ 𝑋 )
38	37	biantrurd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑔 ∈ 𝐾 ) → ( 𝑠 = ran ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) − 𝑔 ) ) ↔ ( 𝑔 ∈ 𝑋 ∧ 𝑠 = ran ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) − 𝑔 ) ) ) ) )
39	35 38	bitrid	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑔 ∈ 𝐾 ) → ( ran ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) − 𝑔 ) ) = 𝑠 ↔ ( 𝑔 ∈ 𝑋 ∧ 𝑠 = ran ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) − 𝑔 ) ) ) ) )
40		simpr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑔 ∈ 𝐾 ) → 𝑔 ∈ 𝐾 )
41		simplr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑔 ∈ 𝐾 ) → 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) )
42		simpr	⊢ ( ( 𝑥 = 𝑔 ∧ 𝑦 = 𝑠 ) → 𝑦 = 𝑠 )
43		simpl	⊢ ( ( 𝑥 = 𝑔 ∧ 𝑦 = 𝑠 ) → 𝑥 = 𝑔 )
44	43	oveq1d	⊢ ( ( 𝑥 = 𝑔 ∧ 𝑦 = 𝑠 ) → ( 𝑥 + 𝑧 ) = ( 𝑔 + 𝑧 ) )
45	44 43	oveq12d	⊢ ( ( 𝑥 = 𝑔 ∧ 𝑦 = 𝑠 ) → ( ( 𝑥 + 𝑧 ) − 𝑥 ) = ( ( 𝑔 + 𝑧 ) − 𝑔 ) )
46	42 45	mpteq12dv	⊢ ( ( 𝑥 = 𝑔 ∧ 𝑦 = 𝑠 ) → ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) = ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) − 𝑔 ) ) )
47	46	rneqd	⊢ ( ( 𝑥 = 𝑔 ∧ 𝑦 = 𝑠 ) → ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) = ran ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) − 𝑔 ) ) )
48		vex	⊢ 𝑠 ∈ V
49	48	mptex	⊢ ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) − 𝑔 ) ) ∈ V
50	49	rnex	⊢ ran ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) − 𝑔 ) ) ∈ V
51	47 8 50	ovmpoa	⊢ ( ( 𝑔 ∈ 𝐾 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) → ( 𝑔 ⊕ 𝑠 ) = ran ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) − 𝑔 ) ) )
52	40 41 51	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑔 ∈ 𝐾 ) → ( 𝑔 ⊕ 𝑠 ) = ran ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) − 𝑔 ) ) )
53	52	eqeq1d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑔 ∈ 𝐾 ) → ( ( 𝑔 ⊕ 𝑠 ) = 𝑠 ↔ ran ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) − 𝑔 ) ) = 𝑠 ) )
54		slwsubg	⊢ ( 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) → 𝑠 ∈ ( SubGrp ‘ 𝐺 ) )
55	54	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑔 ∈ 𝐾 ) → 𝑠 ∈ ( SubGrp ‘ 𝐺 ) )
56		eqid	⊢ ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) − 𝑔 ) ) = ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) − 𝑔 ) )
57	1 5 6 56 9	conjnmzb	⊢ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑔 ∈ 𝑁 ↔ ( 𝑔 ∈ 𝑋 ∧ 𝑠 = ran ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) − 𝑔 ) ) ) ) )
58	55 57	syl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑔 ∈ 𝐾 ) → ( 𝑔 ∈ 𝑁 ↔ ( 𝑔 ∈ 𝑋 ∧ 𝑠 = ran ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) − 𝑔 ) ) ) ) )
59	39 53 58	3bitr4d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑔 ∈ 𝐾 ) → ( ( 𝑔 ⊕ 𝑠 ) = 𝑠 ↔ 𝑔 ∈ 𝑁 ) )
60	59	ralbidva	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) → ( ∀ 𝑔 ∈ 𝐾 ( 𝑔 ⊕ 𝑠 ) = 𝑠 ↔ ∀ 𝑔 ∈ 𝐾 𝑔 ∈ 𝑁 ) )
61		dfss3	⊢ ( 𝐾 ⊆ 𝑁 ↔ ∀ 𝑔 ∈ 𝐾 𝑔 ∈ 𝑁 )
62	60 61	bitr4di	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) → ( ∀ 𝑔 ∈ 𝐾 ( 𝑔 ⊕ 𝑠 ) = 𝑠 ↔ 𝐾 ⊆ 𝑁 ) )
63	18	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) → 𝐾 = ( Base ‘ ( 𝐺 ↾_s 𝐾 ) ) )
64	63	raleqdv	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) → ( ∀ 𝑔 ∈ 𝐾 ( 𝑔 ⊕ 𝑠 ) = 𝑠 ↔ ∀ 𝑔 ∈ ( Base ‘ ( 𝐺 ↾_s 𝐾 ) ) ( 𝑔 ⊕ 𝑠 ) = 𝑠 ) )
65		eqid	⊢ ( Base ‘ ( 𝐺 ↾_s 𝑁 ) ) = ( Base ‘ ( 𝐺 ↾_s 𝑁 ) )
66	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ⊆ 𝑁 ) → 𝐺 ∈ Grp )
67	9 1 5	nmzsubg	⊢ ( 𝐺 ∈ Grp → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
68	66 67	syl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ⊆ 𝑁 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
69		eqid	⊢ ( 𝐺 ↾_s 𝑁 ) = ( 𝐺 ↾_s 𝑁 )
70	69	subgbas	⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → 𝑁 = ( Base ‘ ( 𝐺 ↾_s 𝑁 ) ) )
71	68 70	syl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ⊆ 𝑁 ) → 𝑁 = ( Base ‘ ( 𝐺 ↾_s 𝑁 ) ) )
72	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ⊆ 𝑁 ) → 𝑋 ∈ Fin )
73	1	subgss	⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → 𝑁 ⊆ 𝑋 )
74	68 73	syl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ⊆ 𝑁 ) → 𝑁 ⊆ 𝑋 )
75	72 74	ssfid	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ⊆ 𝑁 ) → 𝑁 ∈ Fin )
76	71 75	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ⊆ 𝑁 ) → ( Base ‘ ( 𝐺 ↾_s 𝑁 ) ) ∈ Fin )
77	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ⊆ 𝑁 ) → 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) )
78		simpr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ⊆ 𝑁 ) → 𝐾 ⊆ 𝑁 )
79	69	subgslw	⊢ ( ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ⊆ 𝑁 ) → 𝐾 ∈ ( 𝑃 pSyl ( 𝐺 ↾_s 𝑁 ) ) )
80	68 77 78 79	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ⊆ 𝑁 ) → 𝐾 ∈ ( 𝑃 pSyl ( 𝐺 ↾_s 𝑁 ) ) )
81		simplr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ⊆ 𝑁 ) → 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) )
82	54	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ⊆ 𝑁 ) → 𝑠 ∈ ( SubGrp ‘ 𝐺 ) )
83	9 1 5	ssnmz	⊢ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → 𝑠 ⊆ 𝑁 )
84	82 83	syl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ⊆ 𝑁 ) → 𝑠 ⊆ 𝑁 )
85	69	subgslw	⊢ ( ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝑠 ⊆ 𝑁 ) → 𝑠 ∈ ( 𝑃 pSyl ( 𝐺 ↾_s 𝑁 ) ) )
86	68 81 84 85	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ⊆ 𝑁 ) → 𝑠 ∈ ( 𝑃 pSyl ( 𝐺 ↾_s 𝑁 ) ) )
87	1	fvexi	⊢ 𝑋 ∈ V
88	9 87	rabex2	⊢ 𝑁 ∈ V
89	69 5	ressplusg	⊢ ( 𝑁 ∈ V → + = ( +_g ‘ ( 𝐺 ↾_s 𝑁 ) ) )
90	88 89	ax-mp	⊢ + = ( +_g ‘ ( 𝐺 ↾_s 𝑁 ) )
91		eqid	⊢ ( -_g ‘ ( 𝐺 ↾_s 𝑁 ) ) = ( -_g ‘ ( 𝐺 ↾_s 𝑁 ) )
92	65 76 80 86 90 91	sylow2	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ⊆ 𝑁 ) → ∃ 𝑔 ∈ ( Base ‘ ( 𝐺 ↾_s 𝑁 ) ) 𝐾 = ran ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) ( -_g ‘ ( 𝐺 ↾_s 𝑁 ) ) 𝑔 ) ) )
93	9 1 5 69	nmznsg	⊢ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → 𝑠 ∈ ( NrmSGrp ‘ ( 𝐺 ↾_s 𝑁 ) ) )
94	82 93	syl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ⊆ 𝑁 ) → 𝑠 ∈ ( NrmSGrp ‘ ( 𝐺 ↾_s 𝑁 ) ) )
95		eqid	⊢ ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) ( -_g ‘ ( 𝐺 ↾_s 𝑁 ) ) 𝑔 ) ) = ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) ( -_g ‘ ( 𝐺 ↾_s 𝑁 ) ) 𝑔 ) )
96	65 90 91 95	conjnsg	⊢ ( ( 𝑠 ∈ ( NrmSGrp ‘ ( 𝐺 ↾_s 𝑁 ) ) ∧ 𝑔 ∈ ( Base ‘ ( 𝐺 ↾_s 𝑁 ) ) ) → 𝑠 = ran ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) ( -_g ‘ ( 𝐺 ↾_s 𝑁 ) ) 𝑔 ) ) )
97	94 96	sylan	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ⊆ 𝑁 ) ∧ 𝑔 ∈ ( Base ‘ ( 𝐺 ↾_s 𝑁 ) ) ) → 𝑠 = ran ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) ( -_g ‘ ( 𝐺 ↾_s 𝑁 ) ) 𝑔 ) ) )
98		eqeq2	⊢ ( 𝐾 = ran ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) ( -_g ‘ ( 𝐺 ↾_s 𝑁 ) ) 𝑔 ) ) → ( 𝑠 = 𝐾 ↔ 𝑠 = ran ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) ( -_g ‘ ( 𝐺 ↾_s 𝑁 ) ) 𝑔 ) ) ) )
99	97 98	syl5ibrcom	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ⊆ 𝑁 ) ∧ 𝑔 ∈ ( Base ‘ ( 𝐺 ↾_s 𝑁 ) ) ) → ( 𝐾 = ran ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) ( -_g ‘ ( 𝐺 ↾_s 𝑁 ) ) 𝑔 ) ) → 𝑠 = 𝐾 ) )
100	99	rexlimdva	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ⊆ 𝑁 ) → ( ∃ 𝑔 ∈ ( Base ‘ ( 𝐺 ↾_s 𝑁 ) ) 𝐾 = ran ( 𝑧 ∈ 𝑠 ↦ ( ( 𝑔 + 𝑧 ) ( -_g ‘ ( 𝐺 ↾_s 𝑁 ) ) 𝑔 ) ) → 𝑠 = 𝐾 ) )
101	92 100	mpd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ⊆ 𝑁 ) → 𝑠 = 𝐾 )
102		simpr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑠 = 𝐾 ) → 𝑠 = 𝐾 )
103	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑠 = 𝐾 ) → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
104	102 103	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑠 = 𝐾 ) → 𝑠 ∈ ( SubGrp ‘ 𝐺 ) )
105	104 83	syl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑠 = 𝐾 ) → 𝑠 ⊆ 𝑁 )
106	102 105	eqsstrrd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑠 = 𝐾 ) → 𝐾 ⊆ 𝑁 )
107	101 106	impbida	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) → ( 𝐾 ⊆ 𝑁 ↔ 𝑠 = 𝐾 ) )
108	62 64 107	3bitr3d	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ) → ( ∀ 𝑔 ∈ ( Base ‘ ( 𝐺 ↾_s 𝐾 ) ) ( 𝑔 ⊕ 𝑠 ) = 𝑠 ↔ 𝑠 = 𝐾 ) )
109	108	rabbidva	⊢ ( 𝜑 → { 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ∣ ∀ 𝑔 ∈ ( Base ‘ ( 𝐺 ↾_s 𝐾 ) ) ( 𝑔 ⊕ 𝑠 ) = 𝑠 } = { 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ∣ 𝑠 = 𝐾 } )
110		rabsn	⊢ ( 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) → { 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ∣ 𝑠 = 𝐾 } = { 𝐾 } )
111	7 110	syl	⊢ ( 𝜑 → { 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ∣ 𝑠 = 𝐾 } = { 𝐾 } )
112	109 111	eqtrd	⊢ ( 𝜑 → { 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ∣ ∀ 𝑔 ∈ ( Base ‘ ( 𝐺 ↾_s 𝐾 ) ) ( 𝑔 ⊕ 𝑠 ) = 𝑠 } = { 𝐾 } )
113	112	fveq2d	⊢ ( 𝜑 → ( ♯ ‘ { 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ∣ ∀ 𝑔 ∈ ( Base ‘ ( 𝐺 ↾_s 𝐾 ) ) ( 𝑔 ⊕ 𝑠 ) = 𝑠 } ) = ( ♯ ‘ { 𝐾 } ) )
114		hashsng	⊢ ( 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) → ( ♯ ‘ { 𝐾 } ) = 1 )
115	7 114	syl	⊢ ( 𝜑 → ( ♯ ‘ { 𝐾 } ) = 1 )
116	113 115	eqtrd	⊢ ( 𝜑 → ( ♯ ‘ { 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ∣ ∀ 𝑔 ∈ ( Base ‘ ( 𝐺 ↾_s 𝐾 ) ) ( 𝑔 ⊕ 𝑠 ) = 𝑠 } ) = 1 )
117	116	oveq2d	⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) − ( ♯ ‘ { 𝑠 ∈ ( 𝑃 pSyl 𝐺 ) ∣ ∀ 𝑔 ∈ ( Base ‘ ( 𝐺 ↾_s 𝐾 ) ) ( 𝑔 ⊕ 𝑠 ) = 𝑠 } ) ) = ( ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) − 1 ) )
118	34 117	breqtrd	⊢ ( 𝜑 → 𝑃 ∥ ( ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) − 1 ) )
119		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
120	4 119	syl	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
121		hashcl	⊢ ( ( 𝑃 pSyl 𝐺 ) ∈ Fin → ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) ∈ ℕ₀ )
122	31 121	syl	⊢ ( 𝜑 → ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) ∈ ℕ₀ )
123	122	nn0zd	⊢ ( 𝜑 → ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) ∈ ℤ )
124		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
125		moddvds	⊢ ( ( 𝑃 ∈ ℕ ∧ ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) ↔ 𝑃 ∥ ( ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) − 1 ) ) )
126	120 123 124 125	syl3anc	⊢ ( 𝜑 → ( ( ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) ↔ 𝑃 ∥ ( ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) − 1 ) ) )
127	118 126	mpbird	⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) )
128		prmuz2	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ_≥ ‘ 2 ) )
129		eluz2b2	⊢ ( 𝑃 ∈ ( ℤ_≥ ‘ 2 ) ↔ ( 𝑃 ∈ ℕ ∧ 1 < 𝑃 ) )
130		nnre	⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℝ )
131		1mod	⊢ ( ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) → ( 1 mod 𝑃 ) = 1 )
132	130 131	sylan	⊢ ( ( 𝑃 ∈ ℕ ∧ 1 < 𝑃 ) → ( 1 mod 𝑃 ) = 1 )
133	129 132	sylbi	⊢ ( 𝑃 ∈ ( ℤ_≥ ‘ 2 ) → ( 1 mod 𝑃 ) = 1 )
134	4 128 133	3syl	⊢ ( 𝜑 → ( 1 mod 𝑃 ) = 1 )
135	127 134	eqtrd	⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) mod 𝑃 ) = 1 )

Metamath Proof Explorer

Theorem sylow3lem6

Proof