Metamath Proof Explorer

Theorem 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 𝐺 ) ) ∈ ℕ0 )
122 31 121 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) ∈ ℕ0 )
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 )