Step |
Hyp |
Ref |
Expression |
1 |
|
sylow3.x |
⊢ 𝑋 = ( Base ‘ 𝐺 ) |
2 |
|
sylow3.g |
⊢ ( 𝜑 → 𝐺 ∈ Grp ) |
3 |
|
sylow3.xf |
⊢ ( 𝜑 → 𝑋 ∈ Fin ) |
4 |
|
sylow3.p |
⊢ ( 𝜑 → 𝑃 ∈ ℙ ) |
5 |
|
sylow3lem1.a |
⊢ + = ( +g ‘ 𝐺 ) |
6 |
|
sylow3lem1.d |
⊢ − = ( -g ‘ 𝐺 ) |
7 |
|
sylow3lem1.m |
⊢ ⊕ = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) ) |
8 |
|
sylow3lem2.k |
⊢ ( 𝜑 → 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ) |
9 |
|
sylow3lem2.h |
⊢ 𝐻 = { 𝑢 ∈ 𝑋 ∣ ( 𝑢 ⊕ 𝐾 ) = 𝐾 } |
10 |
|
sylow3lem2.n |
⊢ 𝑁 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝐾 ↔ ( 𝑦 + 𝑥 ) ∈ 𝐾 ) } |
11 |
|
pwfi |
⊢ ( 𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin ) |
12 |
3 11
|
sylib |
⊢ ( 𝜑 → 𝒫 𝑋 ∈ Fin ) |
13 |
|
slwsubg |
⊢ ( 𝑥 ∈ ( 𝑃 pSyl 𝐺 ) → 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) |
14 |
1
|
subgss |
⊢ ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) → 𝑥 ⊆ 𝑋 ) |
15 |
13 14
|
syl |
⊢ ( 𝑥 ∈ ( 𝑃 pSyl 𝐺 ) → 𝑥 ⊆ 𝑋 ) |
16 |
13 15
|
elpwd |
⊢ ( 𝑥 ∈ ( 𝑃 pSyl 𝐺 ) → 𝑥 ∈ 𝒫 𝑋 ) |
17 |
16
|
ssriv |
⊢ ( 𝑃 pSyl 𝐺 ) ⊆ 𝒫 𝑋 |
18 |
|
ssfi |
⊢ ( ( 𝒫 𝑋 ∈ Fin ∧ ( 𝑃 pSyl 𝐺 ) ⊆ 𝒫 𝑋 ) → ( 𝑃 pSyl 𝐺 ) ∈ Fin ) |
19 |
12 17 18
|
sylancl |
⊢ ( 𝜑 → ( 𝑃 pSyl 𝐺 ) ∈ Fin ) |
20 |
|
hashcl |
⊢ ( ( 𝑃 pSyl 𝐺 ) ∈ Fin → ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) ∈ ℕ0 ) |
21 |
19 20
|
syl |
⊢ ( 𝜑 → ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) ∈ ℕ0 ) |
22 |
21
|
nn0cnd |
⊢ ( 𝜑 → ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) ∈ ℂ ) |
23 |
10 1 5
|
nmzsubg |
⊢ ( 𝐺 ∈ Grp → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) ) |
24 |
|
eqid |
⊢ ( 𝐺 ~QG 𝑁 ) = ( 𝐺 ~QG 𝑁 ) |
25 |
1 24
|
eqger |
⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ~QG 𝑁 ) Er 𝑋 ) |
26 |
2 23 25
|
3syl |
⊢ ( 𝜑 → ( 𝐺 ~QG 𝑁 ) Er 𝑋 ) |
27 |
26
|
qsss |
⊢ ( 𝜑 → ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ⊆ 𝒫 𝑋 ) |
28 |
12 27
|
ssfid |
⊢ ( 𝜑 → ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ∈ Fin ) |
29 |
|
hashcl |
⊢ ( ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ∈ Fin → ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) ∈ ℕ0 ) |
30 |
28 29
|
syl |
⊢ ( 𝜑 → ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) ∈ ℕ0 ) |
31 |
30
|
nn0cnd |
⊢ ( 𝜑 → ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) ∈ ℂ ) |
32 |
2 23
|
syl |
⊢ ( 𝜑 → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) ) |
33 |
|
eqid |
⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 ) |
34 |
33
|
subg0cl |
⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝑁 ) |
35 |
|
ne0i |
⊢ ( ( 0g ‘ 𝐺 ) ∈ 𝑁 → 𝑁 ≠ ∅ ) |
36 |
32 34 35
|
3syl |
⊢ ( 𝜑 → 𝑁 ≠ ∅ ) |
37 |
1
|
subgss |
⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → 𝑁 ⊆ 𝑋 ) |
38 |
2 23 37
|
3syl |
⊢ ( 𝜑 → 𝑁 ⊆ 𝑋 ) |
39 |
3 38
|
ssfid |
⊢ ( 𝜑 → 𝑁 ∈ Fin ) |
40 |
|
hashnncl |
⊢ ( 𝑁 ∈ Fin → ( ( ♯ ‘ 𝑁 ) ∈ ℕ ↔ 𝑁 ≠ ∅ ) ) |
41 |
39 40
|
syl |
⊢ ( 𝜑 → ( ( ♯ ‘ 𝑁 ) ∈ ℕ ↔ 𝑁 ≠ ∅ ) ) |
42 |
36 41
|
mpbird |
⊢ ( 𝜑 → ( ♯ ‘ 𝑁 ) ∈ ℕ ) |
43 |
42
|
nncnd |
⊢ ( 𝜑 → ( ♯ ‘ 𝑁 ) ∈ ℂ ) |
44 |
42
|
nnne0d |
⊢ ( 𝜑 → ( ♯ ‘ 𝑁 ) ≠ 0 ) |
45 |
1 2 3 4 5 6 7
|
sylow3lem1 |
⊢ ( 𝜑 → ⊕ ∈ ( 𝐺 GrpAct ( 𝑃 pSyl 𝐺 ) ) ) |
46 |
|
eqid |
⊢ ( 𝐺 ~QG 𝐻 ) = ( 𝐺 ~QG 𝐻 ) |
47 |
|
eqid |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } |
48 |
1 9 46 47
|
orbsta2 |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ 𝑋 ) = ( ( ♯ ‘ [ 𝐾 ] { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } ) · ( ♯ ‘ 𝐻 ) ) ) |
49 |
45 8 3 48
|
syl21anc |
⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) = ( ( ♯ ‘ [ 𝐾 ] { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } ) · ( ♯ ‘ 𝐻 ) ) ) |
50 |
1 24 32 3
|
lagsubg2 |
⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) = ( ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) · ( ♯ ‘ 𝑁 ) ) ) |
51 |
47 1
|
gaorber |
⊢ ( ⊕ ∈ ( 𝐺 GrpAct ( 𝑃 pSyl 𝐺 ) ) → { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } Er ( 𝑃 pSyl 𝐺 ) ) |
52 |
45 51
|
syl |
⊢ ( 𝜑 → { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } Er ( 𝑃 pSyl 𝐺 ) ) |
53 |
52
|
ecss |
⊢ ( 𝜑 → [ 𝐾 ] { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } ⊆ ( 𝑃 pSyl 𝐺 ) ) |
54 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝑃 pSyl 𝐺 ) ) → 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ) |
55 |
|
simpr |
⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝑃 pSyl 𝐺 ) ) → ℎ ∈ ( 𝑃 pSyl 𝐺 ) ) |
56 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝑃 pSyl 𝐺 ) ) → 𝑋 ∈ Fin ) |
57 |
1 56 55 54 5 6
|
sylow2 |
⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝑃 pSyl 𝐺 ) ) → ∃ 𝑢 ∈ 𝑋 ℎ = ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) |
58 |
|
eqcom |
⊢ ( ( 𝑢 ⊕ 𝐾 ) = ℎ ↔ ℎ = ( 𝑢 ⊕ 𝐾 ) ) |
59 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑢 ∈ 𝑋 ) → 𝑢 ∈ 𝑋 ) |
60 |
54
|
adantr |
⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑢 ∈ 𝑋 ) → 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ) |
61 |
|
mptexg |
⊢ ( 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) → ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ∈ V ) |
62 |
|
rnexg |
⊢ ( ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ∈ V → ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ∈ V ) |
63 |
60 61 62
|
3syl |
⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑢 ∈ 𝑋 ) → ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ∈ V ) |
64 |
|
simpr |
⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝐾 ) → 𝑦 = 𝐾 ) |
65 |
|
simpl |
⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝐾 ) → 𝑥 = 𝑢 ) |
66 |
65
|
oveq1d |
⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝐾 ) → ( 𝑥 + 𝑧 ) = ( 𝑢 + 𝑧 ) ) |
67 |
66 65
|
oveq12d |
⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝐾 ) → ( ( 𝑥 + 𝑧 ) − 𝑥 ) = ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) |
68 |
64 67
|
mpteq12dv |
⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝐾 ) → ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) = ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) |
69 |
68
|
rneqd |
⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝐾 ) → ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) = ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) |
70 |
69 7
|
ovmpoga |
⊢ ( ( 𝑢 ∈ 𝑋 ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ∈ V ) → ( 𝑢 ⊕ 𝐾 ) = ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) |
71 |
59 60 63 70
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑢 ∈ 𝑋 ) → ( 𝑢 ⊕ 𝐾 ) = ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) |
72 |
71
|
eqeq2d |
⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑢 ∈ 𝑋 ) → ( ℎ = ( 𝑢 ⊕ 𝐾 ) ↔ ℎ = ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) ) |
73 |
58 72
|
syl5bb |
⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( 𝑃 pSyl 𝐺 ) ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑢 ⊕ 𝐾 ) = ℎ ↔ ℎ = ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) ) |
74 |
73
|
rexbidva |
⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝑃 pSyl 𝐺 ) ) → ( ∃ 𝑢 ∈ 𝑋 ( 𝑢 ⊕ 𝐾 ) = ℎ ↔ ∃ 𝑢 ∈ 𝑋 ℎ = ran ( 𝑧 ∈ 𝐾 ↦ ( ( 𝑢 + 𝑧 ) − 𝑢 ) ) ) ) |
75 |
57 74
|
mpbird |
⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝑃 pSyl 𝐺 ) ) → ∃ 𝑢 ∈ 𝑋 ( 𝑢 ⊕ 𝐾 ) = ℎ ) |
76 |
47
|
gaorb |
⊢ ( 𝐾 { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } ℎ ↔ ( 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ ℎ ∈ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑢 ∈ 𝑋 ( 𝑢 ⊕ 𝐾 ) = ℎ ) ) |
77 |
54 55 75 76
|
syl3anbrc |
⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝑃 pSyl 𝐺 ) ) → 𝐾 { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } ℎ ) |
78 |
|
elecg |
⊢ ( ( ℎ ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ) → ( ℎ ∈ [ 𝐾 ] { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } ↔ 𝐾 { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } ℎ ) ) |
79 |
55 54 78
|
syl2anc |
⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝑃 pSyl 𝐺 ) ) → ( ℎ ∈ [ 𝐾 ] { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } ↔ 𝐾 { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } ℎ ) ) |
80 |
77 79
|
mpbird |
⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝑃 pSyl 𝐺 ) ) → ℎ ∈ [ 𝐾 ] { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } ) |
81 |
53 80
|
eqelssd |
⊢ ( 𝜑 → [ 𝐾 ] { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } = ( 𝑃 pSyl 𝐺 ) ) |
82 |
81
|
fveq2d |
⊢ ( 𝜑 → ( ♯ ‘ [ 𝐾 ] { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } ) = ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) ) |
83 |
1 2 3 4 5 6 7 8 9 10
|
sylow3lem2 |
⊢ ( 𝜑 → 𝐻 = 𝑁 ) |
84 |
83
|
fveq2d |
⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) = ( ♯ ‘ 𝑁 ) ) |
85 |
82 84
|
oveq12d |
⊢ ( 𝜑 → ( ( ♯ ‘ [ 𝐾 ] { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑃 pSyl 𝐺 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } ) · ( ♯ ‘ 𝐻 ) ) = ( ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) · ( ♯ ‘ 𝑁 ) ) ) |
86 |
49 50 85
|
3eqtr3rd |
⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) · ( ♯ ‘ 𝑁 ) ) = ( ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) · ( ♯ ‘ 𝑁 ) ) ) |
87 |
22 31 43 44 86
|
mulcan2ad |
⊢ ( 𝜑 → ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) = ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑁 ) ) ) ) |