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 |
|
slwsubg |
⊢ ( 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ) |
10 |
7 9
|
syl |
⊢ ( 𝜑 → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ) |
11 |
1
|
subgss |
⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → 𝐾 ⊆ 𝑋 ) |
12 |
10 11
|
syl |
⊢ ( 𝜑 → 𝐾 ⊆ 𝑋 ) |
13 |
|
ssid |
⊢ ( 𝑃 pSyl 𝐺 ) ⊆ ( 𝑃 pSyl 𝐺 ) |
14 |
|
resmpo |
⊢ ( ( 𝐾 ⊆ 𝑋 ∧ ( 𝑃 pSyl 𝐺 ) ⊆ ( 𝑃 pSyl 𝐺 ) ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) ) ↾ ( 𝐾 × ( 𝑃 pSyl 𝐺 ) ) ) = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) ) ) |
15 |
12 13 14
|
sylancl |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) ) ↾ ( 𝐾 × ( 𝑃 pSyl 𝐺 ) ) ) = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) ) ) |
16 |
15 8
|
eqtr4di |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) ) ↾ ( 𝐾 × ( 𝑃 pSyl 𝐺 ) ) ) = ⊕ ) |
17 |
|
oveq2 |
⊢ ( 𝑧 = 𝑐 → ( 𝑥 + 𝑧 ) = ( 𝑥 + 𝑐 ) ) |
18 |
17
|
oveq1d |
⊢ ( 𝑧 = 𝑐 → ( ( 𝑥 + 𝑧 ) − 𝑥 ) = ( ( 𝑥 + 𝑐 ) − 𝑥 ) ) |
19 |
18
|
cbvmptv |
⊢ ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) = ( 𝑐 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑐 ) − 𝑥 ) ) |
20 |
|
oveq1 |
⊢ ( 𝑥 = 𝑎 → ( 𝑥 + 𝑐 ) = ( 𝑎 + 𝑐 ) ) |
21 |
|
id |
⊢ ( 𝑥 = 𝑎 → 𝑥 = 𝑎 ) |
22 |
20 21
|
oveq12d |
⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 + 𝑐 ) − 𝑥 ) = ( ( 𝑎 + 𝑐 ) − 𝑎 ) ) |
23 |
22
|
mpteq2dv |
⊢ ( 𝑥 = 𝑎 → ( 𝑐 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑐 ) − 𝑥 ) ) = ( 𝑐 ∈ 𝑦 ↦ ( ( 𝑎 + 𝑐 ) − 𝑎 ) ) ) |
24 |
19 23
|
eqtrid |
⊢ ( 𝑥 = 𝑎 → ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) = ( 𝑐 ∈ 𝑦 ↦ ( ( 𝑎 + 𝑐 ) − 𝑎 ) ) ) |
25 |
24
|
rneqd |
⊢ ( 𝑥 = 𝑎 → ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) = ran ( 𝑐 ∈ 𝑦 ↦ ( ( 𝑎 + 𝑐 ) − 𝑎 ) ) ) |
26 |
|
mpteq1 |
⊢ ( 𝑦 = 𝑏 → ( 𝑐 ∈ 𝑦 ↦ ( ( 𝑎 + 𝑐 ) − 𝑎 ) ) = ( 𝑐 ∈ 𝑏 ↦ ( ( 𝑎 + 𝑐 ) − 𝑎 ) ) ) |
27 |
26
|
rneqd |
⊢ ( 𝑦 = 𝑏 → ran ( 𝑐 ∈ 𝑦 ↦ ( ( 𝑎 + 𝑐 ) − 𝑎 ) ) = ran ( 𝑐 ∈ 𝑏 ↦ ( ( 𝑎 + 𝑐 ) − 𝑎 ) ) ) |
28 |
25 27
|
cbvmpov |
⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) ) = ( 𝑎 ∈ 𝑋 , 𝑏 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑐 ∈ 𝑏 ↦ ( ( 𝑎 + 𝑐 ) − 𝑎 ) ) ) |
29 |
1 2 3 4 5 6 28
|
sylow3lem1 |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) ) ∈ ( 𝐺 GrpAct ( 𝑃 pSyl 𝐺 ) ) ) |
30 |
|
eqid |
⊢ ( 𝐺 ↾s 𝐾 ) = ( 𝐺 ↾s 𝐾 ) |
31 |
30
|
gasubg |
⊢ ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) ) ∈ ( 𝐺 GrpAct ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) ) ↾ ( 𝐾 × ( 𝑃 pSyl 𝐺 ) ) ) ∈ ( ( 𝐺 ↾s 𝐾 ) GrpAct ( 𝑃 pSyl 𝐺 ) ) ) |
32 |
29 10 31
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) ) ↾ ( 𝐾 × ( 𝑃 pSyl 𝐺 ) ) ) ∈ ( ( 𝐺 ↾s 𝐾 ) GrpAct ( 𝑃 pSyl 𝐺 ) ) ) |
33 |
16 32
|
eqeltrrd |
⊢ ( 𝜑 → ⊕ ∈ ( ( 𝐺 ↾s 𝐾 ) GrpAct ( 𝑃 pSyl 𝐺 ) ) ) |