Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . 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 18046 |
. . . . 5
⊢ (𝜑 → ⊕ ∈ ((𝐺 ↾s 𝐾) GrpAct (𝑃 pSyl 𝐺))) |
11 | | eqid 2622 |
. . . . . . 7
⊢ (𝐺 ↾s 𝐾) = (𝐺 ↾s 𝐾) |
12 | 11 | slwpgp 18028 |
. . . . . 6
⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → 𝑃 pGrp (𝐺 ↾s 𝐾)) |
13 | 8, 12 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾s 𝐾)) |
14 | | slwsubg 18025 |
. . . . . . . 8
⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → 𝐾 ∈ (SubGrp‘𝐺)) |
15 | 8, 14 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺)) |
16 | 11 | subgbas 17598 |
. . . . . . 7
⊢ (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 = (Base‘(𝐺 ↾s 𝐾))) |
17 | 15, 16 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐾 = (Base‘(𝐺 ↾s 𝐾))) |
18 | 2 | subgss 17595 |
. . . . . . . 8
⊢ (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 ⊆ 𝑋) |
19 | 15, 18 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ⊆ 𝑋) |
20 | | ssfi 8180 |
. . . . . . 7
⊢ ((𝑋 ∈ Fin ∧ 𝐾 ⊆ 𝑋) → 𝐾 ∈ Fin) |
21 | 4, 19, 20 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ Fin) |
22 | 17, 21 | eqeltrrd 2702 |
. . . . 5
⊢ (𝜑 → (Base‘(𝐺 ↾s 𝐾)) ∈ Fin) |
23 | | pwfi 8261 |
. . . . . . 7
⊢ (𝑋 ∈ Fin ↔ 𝒫
𝑋 ∈
Fin) |
24 | 4, 23 | sylib 208 |
. . . . . 6
⊢ (𝜑 → 𝒫 𝑋 ∈ Fin) |
25 | | slwsubg 18025 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝑃 pSyl 𝐺) → 𝑥 ∈ (SubGrp‘𝐺)) |
26 | 2 | subgss 17595 |
. . . . . . . . 9
⊢ (𝑥 ∈ (SubGrp‘𝐺) → 𝑥 ⊆ 𝑋) |
27 | 25, 26 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑃 pSyl 𝐺) → 𝑥 ⊆ 𝑋) |
28 | | selpw 4165 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝒫 𝑋 ↔ 𝑥 ⊆ 𝑋) |
29 | 27, 28 | sylibr 224 |
. . . . . . 7
⊢ (𝑥 ∈ (𝑃 pSyl 𝐺) → 𝑥 ∈ 𝒫 𝑋) |
30 | 29 | ssriv 3607 |
. . . . . 6
⊢ (𝑃 pSyl 𝐺) ⊆ 𝒫 𝑋 |
31 | | ssfi 8180 |
. . . . . 6
⊢
((𝒫 𝑋 ∈
Fin ∧ (𝑃 pSyl 𝐺) ⊆ 𝒫 𝑋) → (𝑃 pSyl 𝐺) ∈ Fin) |
32 | 24, 30, 31 | sylancl 694 |
. . . . 5
⊢ (𝜑 → (𝑃 pSyl 𝐺) ∈ Fin) |
33 | | eqid 2622 |
. . . . 5
⊢ {𝑠 ∈ (𝑃 pSyl 𝐺) ∣ ∀𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))(𝑔 ⊕ 𝑠) = 𝑠} = {𝑠 ∈ (𝑃 pSyl 𝐺) ∣ ∀𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))(𝑔 ⊕ 𝑠) = 𝑠} |
34 | | eqid 2622 |
. . . . 5
⊢
{〈𝑧, 𝑤〉 ∣ ({𝑧, 𝑤} ⊆ (𝑃 pSyl 𝐺) ∧ ∃ℎ ∈ (Base‘(𝐺 ↾s 𝐾))(ℎ ⊕ 𝑧) = 𝑤)} = {〈𝑧, 𝑤〉 ∣ ({𝑧, 𝑤} ⊆ (𝑃 pSyl 𝐺) ∧ ∃ℎ ∈ (Base‘(𝐺 ↾s 𝐾))(ℎ ⊕ 𝑧) = 𝑤)} |
35 | 1, 10, 13, 22, 32, 33, 34 | sylow2a 18034 |
. . . 4
⊢ (𝜑 → 𝑃 ∥ ((#‘(𝑃 pSyl 𝐺)) − (#‘{𝑠 ∈ (𝑃 pSyl 𝐺) ∣ ∀𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))(𝑔 ⊕ 𝑠) = 𝑠}))) |
36 | | eqcom 2629 |
. . . . . . . . . . . . . 14
⊢ (ran
(𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔)) = 𝑠 ↔ 𝑠 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔))) |
37 | 19 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) → 𝐾 ⊆ 𝑋) |
38 | 37 | sselda 3603 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑔 ∈ 𝐾) → 𝑔 ∈ 𝑋) |
39 | 38 | biantrurd 529 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑔 ∈ 𝐾) → (𝑠 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔)) ↔ (𝑔 ∈ 𝑋 ∧ 𝑠 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔))))) |
40 | 36, 39 | syl5bb 272 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑔 ∈ 𝐾) → (ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔)) = 𝑠 ↔ (𝑔 ∈ 𝑋 ∧ 𝑠 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔))))) |
41 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑔 ∈ 𝐾) → 𝑔 ∈ 𝐾) |
42 | | simplr 792 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑔 ∈ 𝐾) → 𝑠 ∈ (𝑃 pSyl 𝐺)) |
43 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑔 ∧ 𝑦 = 𝑠) → 𝑦 = 𝑠) |
44 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = 𝑔 ∧ 𝑦 = 𝑠) → 𝑥 = 𝑔) |
45 | 44 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = 𝑔 ∧ 𝑦 = 𝑠) → (𝑥 + 𝑧) = (𝑔 + 𝑧)) |
46 | 45, 44 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑔 ∧ 𝑦 = 𝑠) → ((𝑥 + 𝑧) − 𝑥) = ((𝑔 + 𝑧) − 𝑔)) |
47 | 43, 46 | mpteq12dv 4733 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑔 ∧ 𝑦 = 𝑠) → (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔))) |
48 | 47 | rneqd 5353 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝑔 ∧ 𝑦 = 𝑠) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔))) |
49 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑠 ∈ V |
50 | 49 | mptex 6486 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔)) ∈ V |
51 | 50 | rnex 7100 |
. . . . . . . . . . . . . . . 16
⊢ ran
(𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔)) ∈ V |
52 | 48, 9, 51 | ovmpt2a 6791 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ∈ 𝐾 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) → (𝑔 ⊕ 𝑠) = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔))) |
53 | 41, 42, 52 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑔 ∈ 𝐾) → (𝑔 ⊕ 𝑠) = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔))) |
54 | 53 | eqeq1d 2624 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑔 ∈ 𝐾) → ((𝑔 ⊕ 𝑠) = 𝑠 ↔ ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔)) = 𝑠)) |
55 | | slwsubg 18025 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ (𝑃 pSyl 𝐺) → 𝑠 ∈ (SubGrp‘𝐺)) |
56 | 55 | ad2antlr 763 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑔 ∈ 𝐾) → 𝑠 ∈ (SubGrp‘𝐺)) |
57 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔)) = (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔)) |
58 | | sylow3lem6.n |
. . . . . . . . . . . . . . 15
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)} |
59 | 2, 6, 7, 57, 58 | conjnmzb 17695 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ (SubGrp‘𝐺) → (𝑔 ∈ 𝑁 ↔ (𝑔 ∈ 𝑋 ∧ 𝑠 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔))))) |
60 | 56, 59 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑔 ∈ 𝐾) → (𝑔 ∈ 𝑁 ↔ (𝑔 ∈ 𝑋 ∧ 𝑠 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧) − 𝑔))))) |
61 | 40, 54, 60 | 3bitr4d 300 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑔 ∈ 𝐾) → ((𝑔 ⊕ 𝑠) = 𝑠 ↔ 𝑔 ∈ 𝑁)) |
62 | 61 | ralbidva 2985 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) → (∀𝑔 ∈ 𝐾 (𝑔 ⊕ 𝑠) = 𝑠 ↔ ∀𝑔 ∈ 𝐾 𝑔 ∈ 𝑁)) |
63 | | dfss3 3592 |
. . . . . . . . . . 11
⊢ (𝐾 ⊆ 𝑁 ↔ ∀𝑔 ∈ 𝐾 𝑔 ∈ 𝑁) |
64 | 62, 63 | syl6bbr 278 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) → (∀𝑔 ∈ 𝐾 (𝑔 ⊕ 𝑠) = 𝑠 ↔ 𝐾 ⊆ 𝑁)) |
65 | 17 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) → 𝐾 = (Base‘(𝐺 ↾s 𝐾))) |
66 | 65 | raleqdv 3144 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) → (∀𝑔 ∈ 𝐾 (𝑔 ⊕ 𝑠) = 𝑠 ↔ ∀𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))(𝑔 ⊕ 𝑠) = 𝑠)) |
67 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(Base‘(𝐺
↾s 𝑁)) =
(Base‘(𝐺
↾s 𝑁)) |
68 | 3 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝐺 ∈ Grp) |
69 | 58, 2, 6 | nmzsubg 17635 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Grp → 𝑁 ∈ (SubGrp‘𝐺)) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑁 ∈ (SubGrp‘𝐺)) |
71 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ↾s 𝑁) = (𝐺 ↾s 𝑁) |
72 | 71 | subgbas 17598 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ (SubGrp‘𝐺) → 𝑁 = (Base‘(𝐺 ↾s 𝑁))) |
73 | 70, 72 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑁 = (Base‘(𝐺 ↾s 𝑁))) |
74 | 4 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑋 ∈ Fin) |
75 | 2 | subgss 17595 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ (SubGrp‘𝐺) → 𝑁 ⊆ 𝑋) |
76 | 70, 75 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑁 ⊆ 𝑋) |
77 | | ssfi 8180 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ Fin ∧ 𝑁 ⊆ 𝑋) → 𝑁 ∈ Fin) |
78 | 74, 76, 77 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑁 ∈ Fin) |
79 | 73, 78 | eqeltrrd 2702 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → (Base‘(𝐺 ↾s 𝑁)) ∈ Fin) |
80 | 8 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝐾 ∈ (𝑃 pSyl 𝐺)) |
81 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝐾 ⊆ 𝑁) |
82 | 71 | subgslw 18031 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ (SubGrp‘𝐺) ∧ 𝐾 ∈ (𝑃 pSyl 𝐺) ∧ 𝐾 ⊆ 𝑁) → 𝐾 ∈ (𝑃 pSyl (𝐺 ↾s 𝑁))) |
83 | 70, 80, 81, 82 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝐾 ∈ (𝑃 pSyl (𝐺 ↾s 𝑁))) |
84 | | simplr 792 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑠 ∈ (𝑃 pSyl 𝐺)) |
85 | 55 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑠 ∈ (SubGrp‘𝐺)) |
86 | 58, 2, 6 | ssnmz 17636 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ (SubGrp‘𝐺) → 𝑠 ⊆ 𝑁) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑠 ⊆ 𝑁) |
88 | 71 | subgslw 18031 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ (SubGrp‘𝐺) ∧ 𝑠 ∈ (𝑃 pSyl 𝐺) ∧ 𝑠 ⊆ 𝑁) → 𝑠 ∈ (𝑃 pSyl (𝐺 ↾s 𝑁))) |
89 | 70, 84, 87, 88 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑠 ∈ (𝑃 pSyl (𝐺 ↾s 𝑁))) |
90 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝐺)
∈ V |
91 | 2, 90 | eqeltri 2697 |
. . . . . . . . . . . . . . 15
⊢ 𝑋 ∈ V |
92 | 58, 91 | rabex2 4815 |
. . . . . . . . . . . . . 14
⊢ 𝑁 ∈ V |
93 | 71, 6 | ressplusg 15993 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ V → + =
(+g‘(𝐺
↾s 𝑁))) |
94 | 92, 93 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ + =
(+g‘(𝐺
↾s 𝑁)) |
95 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(-g‘(𝐺 ↾s 𝑁)) = (-g‘(𝐺 ↾s 𝑁)) |
96 | 67, 79, 83, 89, 94, 95 | sylow2 18041 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → ∃𝑔 ∈ (Base‘(𝐺 ↾s 𝑁))𝐾 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧)(-g‘(𝐺 ↾s 𝑁))𝑔))) |
97 | 58, 2, 6, 71 | nmznsg 17638 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ (SubGrp‘𝐺) → 𝑠 ∈ (NrmSGrp‘(𝐺 ↾s 𝑁))) |
98 | 85, 97 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑠 ∈ (NrmSGrp‘(𝐺 ↾s 𝑁))) |
99 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧)(-g‘(𝐺 ↾s 𝑁))𝑔)) = (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧)(-g‘(𝐺 ↾s 𝑁))𝑔)) |
100 | 67, 94, 95, 99 | conjnsg 17696 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ (NrmSGrp‘(𝐺 ↾s 𝑁)) ∧ 𝑔 ∈ (Base‘(𝐺 ↾s 𝑁))) → 𝑠 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧)(-g‘(𝐺 ↾s 𝑁))𝑔))) |
101 | 98, 100 | sylan 488 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) ∧ 𝑔 ∈ (Base‘(𝐺 ↾s 𝑁))) → 𝑠 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧)(-g‘(𝐺 ↾s 𝑁))𝑔))) |
102 | | eqeq2 2633 |
. . . . . . . . . . . . . 14
⊢ (𝐾 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧)(-g‘(𝐺 ↾s 𝑁))𝑔)) → (𝑠 = 𝐾 ↔ 𝑠 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧)(-g‘(𝐺 ↾s 𝑁))𝑔)))) |
103 | 101, 102 | syl5ibrcom 237 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) ∧ 𝑔 ∈ (Base‘(𝐺 ↾s 𝑁))) → (𝐾 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧)(-g‘(𝐺 ↾s 𝑁))𝑔)) → 𝑠 = 𝐾)) |
104 | 103 | rexlimdva 3031 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → (∃𝑔 ∈ (Base‘(𝐺 ↾s 𝑁))𝐾 = ran (𝑧 ∈ 𝑠 ↦ ((𝑔 + 𝑧)(-g‘(𝐺 ↾s 𝑁))𝑔)) → 𝑠 = 𝐾)) |
105 | 96, 104 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝐾 ⊆ 𝑁) → 𝑠 = 𝐾) |
106 | | simpr 477 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑠 = 𝐾) → 𝑠 = 𝐾) |
107 | 15 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑠 = 𝐾) → 𝐾 ∈ (SubGrp‘𝐺)) |
108 | 106, 107 | eqeltrd 2701 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑠 = 𝐾) → 𝑠 ∈ (SubGrp‘𝐺)) |
109 | 108, 86 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑠 = 𝐾) → 𝑠 ⊆ 𝑁) |
110 | 106, 109 | eqsstr3d 3640 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑠 = 𝐾) → 𝐾 ⊆ 𝑁) |
111 | 105, 110 | impbida 877 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) → (𝐾 ⊆ 𝑁 ↔ 𝑠 = 𝐾)) |
112 | 64, 66, 111 | 3bitr3d 298 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑃 pSyl 𝐺)) → (∀𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))(𝑔 ⊕ 𝑠) = 𝑠 ↔ 𝑠 = 𝐾)) |
113 | 112 | rabbidva 3188 |
. . . . . . . 8
⊢ (𝜑 → {𝑠 ∈ (𝑃 pSyl 𝐺) ∣ ∀𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))(𝑔 ⊕ 𝑠) = 𝑠} = {𝑠 ∈ (𝑃 pSyl 𝐺) ∣ 𝑠 = 𝐾}) |
114 | | rabsn 4256 |
. . . . . . . . 9
⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → {𝑠 ∈ (𝑃 pSyl 𝐺) ∣ 𝑠 = 𝐾} = {𝐾}) |
115 | 8, 114 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → {𝑠 ∈ (𝑃 pSyl 𝐺) ∣ 𝑠 = 𝐾} = {𝐾}) |
116 | 113, 115 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → {𝑠 ∈ (𝑃 pSyl 𝐺) ∣ ∀𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))(𝑔 ⊕ 𝑠) = 𝑠} = {𝐾}) |
117 | 116 | fveq2d 6195 |
. . . . . 6
⊢ (𝜑 → (#‘{𝑠 ∈ (𝑃 pSyl 𝐺) ∣ ∀𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))(𝑔 ⊕ 𝑠) = 𝑠}) = (#‘{𝐾})) |
118 | | hashsng 13159 |
. . . . . . 7
⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → (#‘{𝐾}) = 1) |
119 | 8, 118 | syl 17 |
. . . . . 6
⊢ (𝜑 → (#‘{𝐾}) = 1) |
120 | 117, 119 | eqtrd 2656 |
. . . . 5
⊢ (𝜑 → (#‘{𝑠 ∈ (𝑃 pSyl 𝐺) ∣ ∀𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))(𝑔 ⊕ 𝑠) = 𝑠}) = 1) |
121 | 120 | oveq2d 6666 |
. . . 4
⊢ (𝜑 → ((#‘(𝑃 pSyl 𝐺)) − (#‘{𝑠 ∈ (𝑃 pSyl 𝐺) ∣ ∀𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))(𝑔 ⊕ 𝑠) = 𝑠})) = ((#‘(𝑃 pSyl 𝐺)) − 1)) |
122 | 35, 121 | breqtrd 4679 |
. . 3
⊢ (𝜑 → 𝑃 ∥ ((#‘(𝑃 pSyl 𝐺)) − 1)) |
123 | | prmnn 15388 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
124 | 5, 123 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑃 ∈ ℕ) |
125 | | hashcl 13147 |
. . . . . 6
⊢ ((𝑃 pSyl 𝐺) ∈ Fin → (#‘(𝑃 pSyl 𝐺)) ∈
ℕ0) |
126 | 32, 125 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘(𝑃 pSyl 𝐺)) ∈
ℕ0) |
127 | 126 | nn0zd 11480 |
. . . 4
⊢ (𝜑 → (#‘(𝑃 pSyl 𝐺)) ∈ ℤ) |
128 | | 1zzd 11408 |
. . . 4
⊢ (𝜑 → 1 ∈
ℤ) |
129 | | moddvds 14991 |
. . . 4
⊢ ((𝑃 ∈ ℕ ∧
(#‘(𝑃 pSyl 𝐺)) ∈ ℤ ∧ 1 ∈
ℤ) → (((#‘(𝑃 pSyl 𝐺)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((#‘(𝑃 pSyl 𝐺)) − 1))) |
130 | 124, 127,
128, 129 | syl3anc 1326 |
. . 3
⊢ (𝜑 → (((#‘(𝑃 pSyl 𝐺)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((#‘(𝑃 pSyl 𝐺)) − 1))) |
131 | 122, 130 | mpbird 247 |
. 2
⊢ (𝜑 → ((#‘(𝑃 pSyl 𝐺)) mod 𝑃) = (1 mod 𝑃)) |
132 | | prmuz2 15408 |
. . 3
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
133 | | eluz2b2 11761 |
. . . 4
⊢ (𝑃 ∈
(ℤ≥‘2) ↔ (𝑃 ∈ ℕ ∧ 1 < 𝑃)) |
134 | | nnre 11027 |
. . . . 5
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℝ) |
135 | | 1mod 12702 |
. . . . 5
⊢ ((𝑃 ∈ ℝ ∧ 1 <
𝑃) → (1 mod 𝑃) = 1) |
136 | 134, 135 | sylan 488 |
. . . 4
⊢ ((𝑃 ∈ ℕ ∧ 1 <
𝑃) → (1 mod 𝑃) = 1) |
137 | 133, 136 | sylbi 207 |
. . 3
⊢ (𝑃 ∈
(ℤ≥‘2) → (1 mod 𝑃) = 1) |
138 | 5, 132, 137 | 3syl 18 |
. 2
⊢ (𝜑 → (1 mod 𝑃) = 1) |
139 | 131, 138 | eqtrd 2656 |
1
⊢ (𝜑 → ((#‘(𝑃 pSyl 𝐺)) mod 𝑃) = 1) |