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 syl5bb ( ( ( 𝜑𝑠 ∈ ( 𝑃 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 )