Step | Hyp | Ref
| Expression |
1 | | sylow3.xf |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ Fin) |
2 | | pwfi 8144 |
. . . . . 6
⊢ (𝑋 ∈ Fin ↔ 𝒫
𝑋 ∈
Fin) |
3 | 1, 2 | sylib 207 |
. . . . 5
⊢ (𝜑 → 𝒫 𝑋 ∈ Fin) |
4 | | slwsubg 17848 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑃 pSyl 𝐺) → 𝑥 ∈ (SubGrp‘𝐺)) |
5 | | sylow3.x |
. . . . . . . . 9
⊢ 𝑋 = (Base‘𝐺) |
6 | 5 | subgss 17418 |
. . . . . . . 8
⊢ (𝑥 ∈ (SubGrp‘𝐺) → 𝑥 ⊆ 𝑋) |
7 | 4, 6 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ (𝑃 pSyl 𝐺) → 𝑥 ⊆ 𝑋) |
8 | | selpw 4115 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 𝑋 ↔ 𝑥 ⊆ 𝑋) |
9 | 7, 8 | sylibr 223 |
. . . . . 6
⊢ (𝑥 ∈ (𝑃 pSyl 𝐺) → 𝑥 ∈ 𝒫 𝑋) |
10 | 9 | ssriv 3572 |
. . . . 5
⊢ (𝑃 pSyl 𝐺) ⊆ 𝒫 𝑋 |
11 | | ssfi 8065 |
. . . . 5
⊢
((𝒫 𝑋 ∈
Fin ∧ (𝑃 pSyl 𝐺) ⊆ 𝒫 𝑋) → (𝑃 pSyl 𝐺) ∈ Fin) |
12 | 3, 10, 11 | sylancl 693 |
. . . 4
⊢ (𝜑 → (𝑃 pSyl 𝐺) ∈ Fin) |
13 | | hashcl 13009 |
. . . 4
⊢ ((𝑃 pSyl 𝐺) ∈ Fin → (#‘(𝑃 pSyl 𝐺)) ∈
ℕ0) |
14 | 12, 13 | syl 17 |
. . 3
⊢ (𝜑 → (#‘(𝑃 pSyl 𝐺)) ∈
ℕ0) |
15 | 14 | nn0cnd 11230 |
. 2
⊢ (𝜑 → (#‘(𝑃 pSyl 𝐺)) ∈ ℂ) |
16 | | sylow3.g |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ Grp) |
17 | | sylow3lem2.n |
. . . . . . . 8
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝐾 ↔ (𝑦 + 𝑥) ∈ 𝐾)} |
18 | | sylow3lem1.a |
. . . . . . . 8
⊢ + =
(+g‘𝐺) |
19 | 17, 5, 18 | nmzsubg 17458 |
. . . . . . 7
⊢ (𝐺 ∈ Grp → 𝑁 ∈ (SubGrp‘𝐺)) |
20 | | eqid 2610 |
. . . . . . . 8
⊢ (𝐺 ~QG 𝑁) = (𝐺 ~QG 𝑁) |
21 | 5, 20 | eqger 17467 |
. . . . . . 7
⊢ (𝑁 ∈ (SubGrp‘𝐺) → (𝐺 ~QG 𝑁) Er 𝑋) |
22 | 16, 19, 21 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → (𝐺 ~QG 𝑁) Er 𝑋) |
23 | 22 | qsss 7695 |
. . . . 5
⊢ (𝜑 → (𝑋 / (𝐺 ~QG 𝑁)) ⊆ 𝒫 𝑋) |
24 | | ssfi 8065 |
. . . . 5
⊢
((𝒫 𝑋 ∈
Fin ∧ (𝑋 /
(𝐺 ~QG
𝑁)) ⊆ 𝒫 𝑋) → (𝑋 / (𝐺 ~QG 𝑁)) ∈ Fin) |
25 | 3, 23, 24 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝑋 / (𝐺 ~QG 𝑁)) ∈ Fin) |
26 | | hashcl 13009 |
. . . 4
⊢ ((𝑋 / (𝐺 ~QG 𝑁)) ∈ Fin → (#‘(𝑋 / (𝐺 ~QG 𝑁))) ∈
ℕ0) |
27 | 25, 26 | syl 17 |
. . 3
⊢ (𝜑 → (#‘(𝑋 / (𝐺 ~QG 𝑁))) ∈
ℕ0) |
28 | 27 | nn0cnd 11230 |
. 2
⊢ (𝜑 → (#‘(𝑋 / (𝐺 ~QG 𝑁))) ∈ ℂ) |
29 | 16, 19 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ (SubGrp‘𝐺)) |
30 | | eqid 2610 |
. . . . . 6
⊢
(0g‘𝐺) = (0g‘𝐺) |
31 | 30 | subg0cl 17425 |
. . . . 5
⊢ (𝑁 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝑁) |
32 | | ne0i 3880 |
. . . . 5
⊢
((0g‘𝐺) ∈ 𝑁 → 𝑁 ≠ ∅) |
33 | 29, 31, 32 | 3syl 18 |
. . . 4
⊢ (𝜑 → 𝑁 ≠ ∅) |
34 | 5 | subgss 17418 |
. . . . . . 7
⊢ (𝑁 ∈ (SubGrp‘𝐺) → 𝑁 ⊆ 𝑋) |
35 | 16, 19, 34 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → 𝑁 ⊆ 𝑋) |
36 | | ssfi 8065 |
. . . . . 6
⊢ ((𝑋 ∈ Fin ∧ 𝑁 ⊆ 𝑋) → 𝑁 ∈ Fin) |
37 | 1, 35, 36 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ Fin) |
38 | | hashnncl 13018 |
. . . . 5
⊢ (𝑁 ∈ Fin →
((#‘𝑁) ∈ ℕ
↔ 𝑁 ≠
∅)) |
39 | 37, 38 | syl 17 |
. . . 4
⊢ (𝜑 → ((#‘𝑁) ∈ ℕ ↔ 𝑁 ≠ ∅)) |
40 | 33, 39 | mpbird 246 |
. . 3
⊢ (𝜑 → (#‘𝑁) ∈ ℕ) |
41 | 40 | nncnd 10913 |
. 2
⊢ (𝜑 → (#‘𝑁) ∈ ℂ) |
42 | 40 | nnne0d 10942 |
. 2
⊢ (𝜑 → (#‘𝑁) ≠ 0) |
43 | | sylow3.p |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ ℙ) |
44 | | sylow3lem1.d |
. . . . 5
⊢ − =
(-g‘𝐺) |
45 | | sylow3lem1.m |
. . . . 5
⊢ ⊕ =
(𝑥 ∈ 𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥))) |
46 | 5, 16, 1, 43, 18, 44, 45 | sylow3lem1 17865 |
. . . 4
⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺))) |
47 | | sylow3lem2.k |
. . . 4
⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺)) |
48 | | sylow3lem2.h |
. . . . 5
⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾} |
49 | | eqid 2610 |
. . . . 5
⊢ (𝐺 ~QG 𝐻) = (𝐺 ~QG 𝐻) |
50 | | eqid 2610 |
. . . . 5
⊢
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} |
51 | 5, 48, 49, 50 | orbsta2 17570 |
. . . 4
⊢ ((( ⊕ ∈
(𝐺 GrpAct (𝑃 pSyl 𝐺)) ∧ 𝐾 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑋 ∈ Fin) → (#‘𝑋) = ((#‘[𝐾]{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) · (#‘𝐻))) |
52 | 46, 47, 1, 51 | syl21anc 1317 |
. . 3
⊢ (𝜑 → (#‘𝑋) = ((#‘[𝐾]{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) · (#‘𝐻))) |
53 | 5, 20, 29, 1 | lagsubg2 17478 |
. . 3
⊢ (𝜑 → (#‘𝑋) = ((#‘(𝑋 / (𝐺 ~QG 𝑁))) · (#‘𝑁))) |
54 | 50, 5 | gaorber 17564 |
. . . . . . . 8
⊢ ( ⊕ ∈
(𝐺 GrpAct (𝑃 pSyl 𝐺)) → {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} Er (𝑃 pSyl 𝐺)) |
55 | 46, 54 | syl 17 |
. . . . . . 7
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} Er (𝑃 pSyl 𝐺)) |
56 | 55 | ecss 7675 |
. . . . . 6
⊢ (𝜑 → [𝐾]{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} ⊆ (𝑃 pSyl 𝐺)) |
57 | 47 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → 𝐾 ∈ (𝑃 pSyl 𝐺)) |
58 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → ℎ ∈ (𝑃 pSyl 𝐺)) |
59 | 1 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → 𝑋 ∈ Fin) |
60 | 5, 59, 58, 57, 18, 44 | sylow2 17864 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → ∃𝑢 ∈ 𝑋 ℎ = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))) |
61 | | eqcom 2617 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ⊕ 𝐾) = ℎ ↔ ℎ = (𝑢 ⊕ 𝐾)) |
62 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → 𝑢 ∈ 𝑋) |
63 | 57 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → 𝐾 ∈ (𝑃 pSyl 𝐺)) |
64 | | mptexg 6389 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V) |
65 | | rnexg 6990 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V → ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V) |
66 | 63, 64, 65 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V) |
67 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → 𝑦 = 𝐾) |
68 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → 𝑥 = 𝑢) |
69 | 68 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → (𝑥 + 𝑧) = (𝑢 + 𝑧)) |
70 | 69, 68 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → ((𝑥 + 𝑧) − 𝑥) = ((𝑢 + 𝑧) − 𝑢)) |
71 | 67, 70 | mpteq12dv 4663 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))) |
72 | 71 | rneqd 5274 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))) |
73 | 72, 45 | ovmpt2ga 6688 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ 𝑋 ∧ 𝐾 ∈ (𝑃 pSyl 𝐺) ∧ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))) |
74 | 62, 63, 66, 73 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))) |
75 | 74 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → (ℎ = (𝑢 ⊕ 𝐾) ↔ ℎ = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))) |
76 | 61, 75 | syl5bb 271 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) ∧ 𝑢 ∈ 𝑋) → ((𝑢 ⊕ 𝐾) = ℎ ↔ ℎ = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))) |
77 | 76 | rexbidva 3031 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → (∃𝑢 ∈ 𝑋 (𝑢 ⊕ 𝐾) = ℎ ↔ ∃𝑢 ∈ 𝑋 ℎ = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))) |
78 | 60, 77 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → ∃𝑢 ∈ 𝑋 (𝑢 ⊕ 𝐾) = ℎ) |
79 | 50 | gaorb 17563 |
. . . . . . . . . 10
⊢ (𝐾{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}ℎ ↔ (𝐾 ∈ (𝑃 pSyl 𝐺) ∧ ℎ ∈ (𝑃 pSyl 𝐺) ∧ ∃𝑢 ∈ 𝑋 (𝑢 ⊕ 𝐾) = ℎ)) |
80 | 57, 58, 78, 79 | syl3anbrc 1239 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → 𝐾{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}ℎ) |
81 | | elecg 7672 |
. . . . . . . . . 10
⊢ ((ℎ ∈ (𝑃 pSyl 𝐺) ∧ 𝐾 ∈ (𝑃 pSyl 𝐺)) → (ℎ ∈ [𝐾]{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} ↔ 𝐾{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}ℎ)) |
82 | 58, 57, 81 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → (ℎ ∈ [𝐾]{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} ↔ 𝐾{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}ℎ)) |
83 | 80, 82 | mpbird 246 |
. . . . . . . 8
⊢ ((𝜑 ∧ ℎ ∈ (𝑃 pSyl 𝐺)) → ℎ ∈ [𝐾]{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) |
84 | 83 | ex 449 |
. . . . . . 7
⊢ (𝜑 → (ℎ ∈ (𝑃 pSyl 𝐺) → ℎ ∈ [𝐾]{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)})) |
85 | 84 | ssrdv 3574 |
. . . . . 6
⊢ (𝜑 → (𝑃 pSyl 𝐺) ⊆ [𝐾]{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) |
86 | 56, 85 | eqssd 3585 |
. . . . 5
⊢ (𝜑 → [𝐾]{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} = (𝑃 pSyl 𝐺)) |
87 | 86 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → (#‘[𝐾]{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) = (#‘(𝑃 pSyl 𝐺))) |
88 | 5, 16, 1, 43, 18, 44, 45, 47, 48, 17 | sylow3lem2 17866 |
. . . . 5
⊢ (𝜑 → 𝐻 = 𝑁) |
89 | 88 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → (#‘𝐻) = (#‘𝑁)) |
90 | 87, 89 | oveq12d 6567 |
. . 3
⊢ (𝜑 → ((#‘[𝐾]{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑃 pSyl 𝐺) ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}) · (#‘𝐻)) = ((#‘(𝑃 pSyl 𝐺)) · (#‘𝑁))) |
91 | 52, 53, 90 | 3eqtr3rd 2653 |
. 2
⊢ (𝜑 → ((#‘(𝑃 pSyl 𝐺)) · (#‘𝑁)) = ((#‘(𝑋 / (𝐺 ~QG 𝑁))) · (#‘𝑁))) |
92 | 15, 28, 41, 42, 91 | mulcan2ad 10542 |
1
⊢ (𝜑 → (#‘(𝑃 pSyl 𝐺)) = (#‘(𝑋 / (𝐺 ~QG 𝑁)))) |