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 X = Base G
sylow3.g φ G Grp
sylow3.xf φ X Fin
sylow3.p φ P
sylow3lem5.a + ˙ = + G
sylow3lem5.d - ˙ = - G
sylow3lem5.k φ K P pSyl G
sylow3lem5.m ˙ = x K , y P pSyl G ran z y x + ˙ z - ˙ x
Assertion sylow3lem5 φ ˙ G 𝑠 K GrpAct P pSyl G

Proof

Step Hyp Ref Expression
1 sylow3.x X = Base G
2 sylow3.g φ G Grp
3 sylow3.xf φ X Fin
4 sylow3.p φ P
5 sylow3lem5.a + ˙ = + G
6 sylow3lem5.d - ˙ = - G
7 sylow3lem5.k φ K P pSyl G
8 sylow3lem5.m ˙ = x K , y P pSyl G ran z y x + ˙ z - ˙ x
9 slwsubg K P pSyl G K SubGrp G
10 7 9 syl φ K SubGrp G
11 1 subgss K SubGrp G K X
12 10 11 syl φ K X
13 ssid P pSyl G P pSyl G
14 resmpo K X P pSyl G P pSyl G x X , y P pSyl G ran z y x + ˙ z - ˙ x K × P pSyl G = x K , y P pSyl G ran z y x + ˙ z - ˙ x
15 12 13 14 sylancl φ x X , y P pSyl G ran z y x + ˙ z - ˙ x K × P pSyl G = x K , y P pSyl G ran z y x + ˙ z - ˙ x
16 15 8 eqtr4di φ x X , y P pSyl G ran z y x + ˙ z - ˙ x K × P pSyl G = ˙
17 oveq2 z = c x + ˙ z = x + ˙ c
18 17 oveq1d z = c x + ˙ z - ˙ x = x + ˙ c - ˙ x
19 18 cbvmptv z y x + ˙ z - ˙ x = c y x + ˙ c - ˙ x
20 oveq1 x = a x + ˙ c = a + ˙ c
21 id x = a x = a
22 20 21 oveq12d x = a x + ˙ c - ˙ x = a + ˙ c - ˙ a
23 22 mpteq2dv x = a c y x + ˙ c - ˙ x = c y a + ˙ c - ˙ a
24 19 23 eqtrid x = a z y x + ˙ z - ˙ x = c y a + ˙ c - ˙ a
25 24 rneqd x = a ran z y x + ˙ z - ˙ x = ran c y a + ˙ c - ˙ a
26 mpteq1 y = b c y a + ˙ c - ˙ a = c b a + ˙ c - ˙ a
27 26 rneqd y = b ran c y a + ˙ c - ˙ a = ran c b a + ˙ c - ˙ a
28 25 27 cbvmpov x X , y P pSyl G ran z y x + ˙ z - ˙ x = a X , b P pSyl G ran c b a + ˙ c - ˙ a
29 1 2 3 4 5 6 28 sylow3lem1 φ x X , y P pSyl G ran z y x + ˙ z - ˙ x G GrpAct P pSyl G
30 eqid G 𝑠 K = G 𝑠 K
31 30 gasubg x X , y P pSyl G ran z y x + ˙ z - ˙ x G GrpAct P pSyl G K SubGrp G x X , y P pSyl G ran z y x + ˙ z - ˙ x K × P pSyl G G 𝑠 K GrpAct P pSyl G
32 29 10 31 syl2anc φ x X , y P pSyl G ran z y x + ˙ z - ˙ x K × P pSyl G G 𝑠 K GrpAct P pSyl G
33 16 32 eqeltrrd φ ˙ G 𝑠 K GrpAct P pSyl G