Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . 5
⊢
(Base‘(𝐺
↾s 𝐾)) =
(Base‘(𝐺
↾s 𝐾)) |
2 | | sylow3.x |
. . . . . 6
⊢ 𝑋 = (Base‘𝐺) |
3 | | sylow3.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ Grp) |
4 | | sylow3.xf |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ Fin) |
5 | | sylow3.p |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℙ) |
6 | | sylow3lem5.a |
. . . . . 6
⊢ + =
(+g‘𝐺) |
7 | | sylow3lem5.d |
. . . . . 6
⊢ − =
(-g‘𝐺) |
8 | | sylow3lem5.k |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺)) |
9 | | sylow3lem5.m |
. . . . . 6
⊢ ⊕ =
(𝑥 ∈ 𝐾, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥))) |
10 | 2, 3, 4, 5, 6, 7, 8, 9 | sylow3lem5 19020 |
. . . . 5
⊢ (𝜑 → ⊕ ∈ ((𝐺 ↾s 𝐾) GrpAct (𝑃 pSyl 𝐺))) |
11 | | eqid 2737 |
. . . . . . 7
⊢ (𝐺 ↾s 𝐾) = (𝐺 ↾s 𝐾) |
12 | 11 | slwpgp 19002 |
. . . . . 6
⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → 𝑃 pGrp (𝐺 ↾s 𝐾)) |
13 | 8, 12 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾s 𝐾)) |
14 | | slwsubg 18999 |
. . . . . . . 8
⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → 𝐾 ∈ (SubGrp‘𝐺)) |
15 | 8, 14 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺)) |
16 | 11 | subgbas 18547 |
. . . . . . 7
⊢ (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 = (Base‘(𝐺 ↾s 𝐾))) |
17 | 15, 16 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐾 = (Base‘(𝐺 ↾s 𝐾))) |
18 | 2 | subgss 18544 |
. . . . . . . 8
⊢ (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 ⊆ 𝑋) |
19 | 15, 18 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ⊆ 𝑋) |
20 | 4, 19 | ssfid 8898 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ Fin) |
21 | 17, 20 | eqeltrrd 2839 |
. . . . 5
⊢ (𝜑 → (Base‘(𝐺 ↾s 𝐾)) ∈ Fin) |
22 | | pwfi 8856 |
. . . . . . 7
⊢ (𝑋 ∈ Fin ↔ 𝒫
𝑋 ∈
Fin) |
23 | 4, 22 | sylib 221 |
. . . . . 6
⊢ (𝜑 → 𝒫 𝑋 ∈ Fin) |
24 | | slwsubg 18999 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑃 pSyl 𝐺) → 𝑥 ∈ (SubGrp‘𝐺)) |
25 | 2 | subgss 18544 |
. . . . . . . . 9
⊢ (𝑥 ∈ (SubGrp‘𝐺) → 𝑥 ⊆ 𝑋) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑃 pSyl 𝐺) → 𝑥 ⊆ 𝑋) |
27 | 24, 26 | elpwd 4521 |
. . . . . . 7
⊢ (𝑥 ∈ (𝑃 pSyl 𝐺) → 𝑥 ∈ 𝒫 𝑋) |
28 | 27 | ssriv 3905 |
. . . . . 6
⊢ (𝑃 pSyl 𝐺) ⊆ 𝒫 𝑋 |
29 | | ssfi 8851 |
. . . . . 6
⊢
((𝒫 𝑋 ∈
Fin ∧ (𝑃 pSyl 𝐺) ⊆ 𝒫 𝑋) → (𝑃 pSyl 𝐺) ∈ Fin) |
30 | 23, 28, 29 | sylancl 589 |
. . . . 5
⊢ (𝜑 → (𝑃 pSyl 𝐺) ∈ Fin) |
31 | | eqid 2737 |
. . . . 5
⊢ {𝑠 ∈ (𝑃 pSyl 𝐺) ∣ ∀𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))(𝑔 ⊕ 𝑠) = 𝑠} = {𝑠 ∈ (𝑃 pSyl 𝐺) ∣ ∀𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))(𝑔 ⊕ 𝑠) = 𝑠} |
32 | | eqid 2737 |
. . . . 5
⊢
{〈𝑧, 𝑤〉 ∣ ({𝑧, 𝑤} ⊆ (𝑃 pSyl 𝐺) ∧ ∃ℎ ∈ (Base‘(𝐺 ↾s 𝐾))(ℎ ⊕ 𝑧) = 𝑤)} = {〈𝑧, 𝑤〉 ∣ ({𝑧, 𝑤} ⊆ (𝑃 pSyl 𝐺) ∧ ∃ℎ ∈ (Base‘(𝐺 ↾s 𝐾))(ℎ ⊕ 𝑧) = 𝑤)} |
33 | 1, 10, 13, 21, 30, 31, 32 | sylow2a 19008 |
. . . 4
⊢ (𝜑 → 𝑃 ∥ ((♯‘(𝑃 pSyl 𝐺)) − (♯‘{𝑠 ∈ (𝑃 pSyl 𝐺) ∣ ∀𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))(𝑔 ⊕ 𝑠) = 𝑠}))) |
34 | | eqcom 2744 |
. . . . . . . . . . . . . 14
⊢ (ran
(𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔)) = 𝑠 ↔ 𝑠 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔))) |
35 | 19 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) → 𝐾 ⊆ 𝑋) |
36 | 35 | sselda 3901 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑔 ∈ 𝐾) → 𝑔 ∈ 𝑋) |
37 | 36 | biantrurd 536 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑔 ∈ 𝐾) → (𝑠 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔)) ↔ (𝑔 ∈ 𝑋 ∧ 𝑠 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔))))) |
38 | 34, 37 | syl5bb 286 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑔 ∈ 𝐾) → (ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔)) = 𝑠 ↔ (𝑔 ∈ 𝑋 ∧ 𝑠 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔))))) |
39 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑔 ∈ 𝐾) → 𝑔 ∈ 𝐾) |
40 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑔 ∈ 𝐾) → 𝑠 ∈ (𝑃 pSyl 𝐺)) |
41 | | simpr 488 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑔 ∧ 𝑦 = 𝑠) → 𝑦 = 𝑠) |
42 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = 𝑔 ∧ 𝑦 = 𝑠) → 𝑥 = 𝑔) |
43 | 42 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = 𝑔 ∧ 𝑦 = 𝑠) → (𝑥 + 𝑧) = (𝑔 + 𝑧)) |
44 | 43, 42 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑔 ∧ 𝑦 = 𝑠) → ((𝑥 + 𝑧) − 𝑥) = ((𝑔 + 𝑧) − 𝑔)) |
45 | 41, 44 | mpteq12dv 5140 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑔 ∧ 𝑦 = 𝑠) → (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔))) |
46 | 45 | rneqd 5807 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝑔 ∧ 𝑦 = 𝑠) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔))) |
47 | | vex 3412 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑠 ∈ V |
48 | 47 | mptex 7039 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔)) ∈ V |
49 | 48 | rnex 7690 |
. . . . . . . . . . . . . . . 16
⊢ ran
(𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔)) ∈ V |
50 | 46, 9, 49 | ovmpoa 7364 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ∈ 𝐾 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) → (𝑔 ⊕ 𝑠) = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔))) |
51 | 39, 40, 50 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑔 ∈ 𝐾) → (𝑔 ⊕ 𝑠) = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔))) |
52 | 51 | eqeq1d 2739 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑔 ∈ 𝐾) → ((𝑔 ⊕ 𝑠) = 𝑠 ↔ ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔)) = 𝑠)) |
53 | | slwsubg 18999 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ (𝑃 pSyl 𝐺) → 𝑠 ∈ (SubGrp‘𝐺)) |
54 | 53 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑔 ∈ 𝐾) → 𝑠 ∈ (SubGrp‘𝐺)) |
55 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔)) = (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔)) |
56 | | sylow3lem6.n |
. . . . . . . . . . . . . . 15
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)} |
57 | 2, 6, 7, 55, 56 | conjnmzb 18657 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ (SubGrp‘𝐺) → (𝑔 ∈ 𝑁 ↔ (𝑔 ∈ 𝑋 ∧ 𝑠 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔))))) |
58 | 54, 57 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑔 ∈ 𝐾) → (𝑔 ∈ 𝑁 ↔ (𝑔 ∈ 𝑋 ∧ 𝑠 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔))))) |
59 | 38, 52, 58 | 3bitr4d 314 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑔 ∈ 𝐾) → ((𝑔 ⊕ 𝑠) = 𝑠 ↔ 𝑔 ∈ 𝑁)) |
60 | 59 | ralbidva 3117 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) → (∀𝑔 ∈ 𝐾 (𝑔 ⊕ 𝑠) = 𝑠 ↔ ∀𝑔 ∈ 𝐾 𝑔 ∈ 𝑁)) |
61 | | dfss3 3888 |
. . . . . . . . . . 11
⊢ (𝐾 ⊆ 𝑁 ↔ ∀𝑔 ∈ 𝐾 𝑔 ∈ 𝑁) |
62 | 60, 61 | bitr4di 292 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) → (∀𝑔 ∈ 𝐾 (𝑔 ⊕ 𝑠) = 𝑠 ↔ 𝐾 ⊆ 𝑁)) |
63 | 17 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) → 𝐾 = (Base‘(𝐺 ↾s 𝐾))) |
64 | 63 | raleqdv 3325 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) → (∀𝑔 ∈ 𝐾 (𝑔 ⊕ 𝑠) = 𝑠 ↔ ∀𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))(𝑔 ⊕ 𝑠) = 𝑠)) |
65 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘(𝐺
↾s 𝑁)) =
(Base‘(𝐺
↾s 𝑁)) |
66 | 3 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝐺 ∈ Grp) |
67 | 56, 2, 6 | nmzsubg 18581 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Grp → 𝑁 ∈ (SubGrp‘𝐺)) |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑁 ∈ (SubGrp‘𝐺)) |
69 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ↾s 𝑁) = (𝐺 ↾s 𝑁) |
70 | 69 | subgbas 18547 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ (SubGrp‘𝐺) → 𝑁 = (Base‘(𝐺 ↾s 𝑁))) |
71 | 68, 70 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑁 = (Base‘(𝐺 ↾s 𝑁))) |
72 | 4 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑋 ∈ Fin) |
73 | 2 | subgss 18544 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ (SubGrp‘𝐺) → 𝑁 ⊆ 𝑋) |
74 | 68, 73 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑁 ⊆ 𝑋) |
75 | 72, 74 | ssfid 8898 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑁 ∈ Fin) |
76 | 71, 75 | eqeltrrd 2839 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → (Base‘(𝐺 ↾s 𝑁)) ∈ Fin) |
77 | 8 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝐾 ∈ (𝑃 pSyl 𝐺)) |
78 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝐾 ⊆ 𝑁) |
79 | 69 | subgslw 19005 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ (SubGrp‘𝐺) ∧ 𝐾 ∈ (𝑃 pSyl 𝐺) ∧ 𝐾 ⊆ 𝑁) → 𝐾 ∈ (𝑃 pSyl (𝐺 ↾s 𝑁))) |
80 | 68, 77, 78, 79 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝐾 ∈ (𝑃 pSyl (𝐺 ↾s 𝑁))) |
81 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑠 ∈ (𝑃 pSyl 𝐺)) |
82 | 53 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑠 ∈ (SubGrp‘𝐺)) |
83 | 56, 2, 6 | ssnmz 18582 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ (SubGrp‘𝐺) → 𝑠 ⊆ 𝑁) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑠 ⊆ 𝑁) |
85 | 69 | subgslw 19005 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ (SubGrp‘𝐺) ∧ 𝑠 ∈ (𝑃 pSyl 𝐺) ∧ 𝑠 ⊆ 𝑁) → 𝑠 ∈ (𝑃 pSyl (𝐺 ↾s 𝑁))) |
86 | 68, 81, 84, 85 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑠 ∈ (𝑃 pSyl (𝐺 ↾s 𝑁))) |
87 | 2 | fvexi 6731 |
. . . . . . . . . . . . . . 15
⊢ 𝑋 ∈ V |
88 | 56, 87 | rabex2 5227 |
. . . . . . . . . . . . . 14
⊢ 𝑁 ∈ V |
89 | 69, 6 | ressplusg 16834 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ V → + =
(+g‘(𝐺
↾s 𝑁))) |
90 | 88, 89 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ + =
(+g‘(𝐺
↾s 𝑁)) |
91 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(-g‘(𝐺 ↾s 𝑁)) = (-g‘(𝐺 ↾s 𝑁)) |
92 | 65, 76, 80, 86, 90, 91 | sylow2 19015 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → ∃𝑔 ∈ (Base‘(𝐺 ↾s 𝑁))𝐾 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧)(-g‘(𝐺 ↾s 𝑁))𝑔))) |
93 | 56, 2, 6, 69 | nmznsg 18584 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ (SubGrp‘𝐺) → 𝑠 ∈ (NrmSGrp‘(𝐺 ↾s 𝑁))) |
94 | 82, 93 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑠 ∈ (NrmSGrp‘(𝐺 ↾s 𝑁))) |
95 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧)(-g‘(𝐺 ↾s 𝑁))𝑔)) = (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧)(-g‘(𝐺 ↾s 𝑁))𝑔)) |
96 | 65, 90, 91, 95 | conjnsg 18658 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ (NrmSGrp‘(𝐺 ↾s 𝑁)) ∧ 𝑔 ∈ (Base‘(𝐺 ↾s 𝑁))) → 𝑠 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧)(-g‘(𝐺 ↾s 𝑁))𝑔))) |
97 | 94, 96 | sylan 583 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) ∧ 𝑔 ∈ (Base‘(𝐺 ↾s 𝑁))) → 𝑠 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧)(-g‘(𝐺 ↾s 𝑁))𝑔))) |
98 | | eqeq2 2749 |
. . . . . . . . . . . . . 14
⊢ (𝐾 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧)(-g‘(𝐺 ↾s 𝑁))𝑔)) → (𝑠 = 𝐾 ↔ 𝑠 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧)(-g‘(𝐺 ↾s 𝑁))𝑔)))) |
99 | 97, 98 | syl5ibrcom 250 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) ∧ 𝑔 ∈ (Base‘(𝐺 ↾s 𝑁))) → (𝐾 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧)(-g‘(𝐺 ↾s 𝑁))𝑔)) → 𝑠 = 𝐾)) |
100 | 99 | rexlimdva 3203 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → (∃𝑔 ∈ (Base‘(𝐺 ↾s 𝑁))𝐾 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧)(-g‘(𝐺 ↾s 𝑁))𝑔)) → 𝑠 = 𝐾)) |
101 | 92, 100 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑠 = 𝐾) |
102 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑠 = 𝐾) → 𝑠 = 𝐾) |
103 | 15 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑠 = 𝐾) → 𝐾 ∈ (SubGrp‘𝐺)) |
104 | 102, 103 | eqeltrd 2838 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑠 = 𝐾) → 𝑠 ∈ (SubGrp‘𝐺)) |
105 | 104, 83 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑠 = 𝐾) → 𝑠 ⊆ 𝑁) |
106 | 102, 105 | eqsstrrd 3940 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑠 = 𝐾) → 𝐾 ⊆ 𝑁) |
107 | 101, 106 | impbida 801 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) → (𝐾 ⊆ 𝑁 ↔ 𝑠 = 𝐾)) |
108 | 62, 64, 107 | 3bitr3d 312 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) → (∀𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))(𝑔 ⊕ 𝑠) = 𝑠 ↔ 𝑠 = 𝐾)) |
109 | 108 | rabbidva 3388 |
. . . . . . . 8
⊢ (𝜑 → {𝑠 ∈ (𝑃 pSyl 𝐺) ∣ ∀𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))(𝑔 ⊕ 𝑠) = 𝑠} = {𝑠 ∈ (𝑃 pSyl 𝐺) ∣ 𝑠 = 𝐾}) |
110 | | rabsn 4637 |
. . . . . . . . 9
⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → {𝑠 ∈ (𝑃 pSyl 𝐺) ∣ 𝑠 = 𝐾} = {𝐾}) |
111 | 8, 110 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → {𝑠 ∈ (𝑃 pSyl 𝐺) ∣ 𝑠 = 𝐾} = {𝐾}) |
112 | 109, 111 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → {𝑠 ∈ (𝑃 pSyl 𝐺) ∣ ∀𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))(𝑔 ⊕ 𝑠) = 𝑠} = {𝐾}) |
113 | 112 | fveq2d 6721 |
. . . . . 6
⊢ (𝜑 → (♯‘{𝑠 ∈ (𝑃 pSyl 𝐺) ∣ ∀𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))(𝑔 ⊕ 𝑠) = 𝑠}) = (♯‘{𝐾})) |
114 | | hashsng 13936 |
. . . . . . 7
⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → (♯‘{𝐾}) = 1) |
115 | 8, 114 | syl 17 |
. . . . . 6
⊢ (𝜑 → (♯‘{𝐾}) = 1) |
116 | 113, 115 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (♯‘{𝑠 ∈ (𝑃 pSyl 𝐺) ∣ ∀𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))(𝑔 ⊕ 𝑠) = 𝑠}) = 1) |
117 | 116 | oveq2d 7229 |
. . . 4
⊢ (𝜑 → ((♯‘(𝑃 pSyl 𝐺)) − (♯‘{𝑠 ∈ (𝑃 pSyl 𝐺) ∣ ∀𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))(𝑔 ⊕ 𝑠) = 𝑠})) = ((♯‘(𝑃 pSyl 𝐺)) − 1)) |
118 | 33, 117 | breqtrd 5079 |
. . 3
⊢ (𝜑 → 𝑃 ∥ ((♯‘(𝑃 pSyl 𝐺)) − 1)) |
119 | | prmnn 16231 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
120 | 5, 119 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑃 ∈ ℕ) |
121 | | hashcl 13923 |
. . . . . 6
⊢ ((𝑃 pSyl 𝐺) ∈ Fin → (♯‘(𝑃 pSyl 𝐺)) ∈
ℕ0) |
122 | 30, 121 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘(𝑃 pSyl 𝐺)) ∈
ℕ0) |
123 | 122 | nn0zd 12280 |
. . . 4
⊢ (𝜑 → (♯‘(𝑃 pSyl 𝐺)) ∈ ℤ) |
124 | | 1zzd 12208 |
. . . 4
⊢ (𝜑 → 1 ∈
ℤ) |
125 | | moddvds 15826 |
. . . 4
⊢ ((𝑃 ∈ ℕ ∧
(♯‘(𝑃 pSyl
𝐺)) ∈ ℤ ∧ 1
∈ ℤ) → (((♯‘(𝑃 pSyl 𝐺)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((♯‘(𝑃 pSyl 𝐺)) − 1))) |
126 | 120, 123,
124, 125 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (((♯‘(𝑃 pSyl 𝐺)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((♯‘(𝑃 pSyl 𝐺)) − 1))) |
127 | 118, 126 | mpbird 260 |
. 2
⊢ (𝜑 → ((♯‘(𝑃 pSyl 𝐺)) mod 𝑃) = (1 mod 𝑃)) |
128 | | prmuz2 16253 |
. . 3
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
129 | | eluz2b2 12517 |
. . . 4
⊢ (𝑃 ∈
(ℤ≥‘2) ↔ (𝑃 ∈ ℕ ∧ 1 < 𝑃)) |
130 | | nnre 11837 |
. . . . 5
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℝ) |
131 | | 1mod 13476 |
. . . . 5
⊢ ((𝑃 ∈ ℝ ∧ 1 <
𝑃) → (1 mod 𝑃) = 1) |
132 | 130, 131 | sylan 583 |
. . . 4
⊢ ((𝑃 ∈ ℕ ∧ 1 <
𝑃) → (1 mod 𝑃) = 1) |
133 | 129, 132 | sylbi 220 |
. . 3
⊢ (𝑃 ∈
(ℤ≥‘2) → (1 mod 𝑃) = 1) |
134 | 5, 128, 133 | 3syl 18 |
. 2
⊢ (𝜑 → (1 mod 𝑃) = 1) |
135 | 127, 134 | eqtrd 2777 |
1
⊢ (𝜑 → ((♯‘(𝑃 pSyl 𝐺)) mod 𝑃) = 1) |