Metamath Proof Explorer


Theorem sylow3lem5

Description: Lemma for sylow3 , second part. Reduce the group action of sylow3lem1 to a given Sylow subgroup. (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypotheses sylow3.x 𝑋 = ( Base ‘ 𝐺 )
sylow3.g ( 𝜑𝐺 ∈ Grp )
sylow3.xf ( 𝜑𝑋 ∈ Fin )
sylow3.p ( 𝜑𝑃 ∈ ℙ )
sylow3lem5.a + = ( +g𝐺 )
sylow3lem5.d = ( -g𝐺 )
sylow3lem5.k ( 𝜑𝐾 ∈ ( 𝑃 pSyl 𝐺 ) )
sylow3lem5.m = ( 𝑥𝐾 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧𝑦 ↦ ( ( 𝑥 + 𝑧 ) 𝑥 ) ) )
Assertion sylow3lem5 ( 𝜑 ∈ ( ( 𝐺s 𝐾 ) GrpAct ( 𝑃 pSyl 𝐺 ) ) )

Proof

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 𝐺 ) ) )