This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sylow2blem2

Description: Lemma for sylow2b . Left multiplication in a subgroup H is a group action on the set of all left cosets of K . (Contributed by Mario Carneiro, 17-Jan-2015)

Ref Expression
Hypotheses sylow2b.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
sylow2b.xf ⊢ ( 𝜑 → 𝑋 ∈ Fin )
sylow2b.h ⊢ ( 𝜑 → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
sylow2b.k ⊢ ( 𝜑 → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
sylow2b.a ⊢ + = ( +g ‘ 𝐺 )
sylow2b.r ⊢ ∼ = ( 𝐺 ~QG 𝐾 )
sylow2b.m ⊢ · = ( 𝑥 ∈ 𝐻 , 𝑦 ∈ ( 𝑋 / ∼ ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) )
Assertion sylow2blem2 ( 𝜑 → · ∈ ( ( 𝐺 ↾s 𝐻 ) GrpAct ( 𝑋 / ∼ ) ) )

Proof

Step Hyp Ref Expression
1 sylow2b.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 sylow2b.xf ⊢ ( 𝜑 → 𝑋 ∈ Fin )
3 sylow2b.h ⊢ ( 𝜑 → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
4 sylow2b.k ⊢ ( 𝜑 → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
5 sylow2b.a ⊢ + = ( +g ‘ 𝐺 )
6 sylow2b.r ⊢ ∼ = ( 𝐺 ~QG 𝐾 )
7 sylow2b.m ⊢ · = ( 𝑥 ∈ 𝐻 , 𝑦 ∈ ( 𝑋 / ∼ ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) )
8 eqid ⊢ ( 𝐺 ↾s 𝐻 ) = ( 𝐺 ↾s 𝐻 )
9 8 subggrp ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ↾s 𝐻 ) ∈ Grp )
10 3 9 syl ⊢ ( 𝜑 → ( 𝐺 ↾s 𝐻 ) ∈ Grp )
11 pwfi ⊢ ( 𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin )
12 2 11 sylib ⊢ ( 𝜑 → 𝒫 𝑋 ∈ Fin )
13 1 6 eqger ⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → ∼ Er 𝑋 )
14 4 13 syl ⊢ ( 𝜑 → ∼ Er 𝑋 )
15 14 qsss ⊢ ( 𝜑 → ( 𝑋 / ∼ ) ⊆ 𝒫 𝑋 )
16 12 15 ssexd ⊢ ( 𝜑 → ( 𝑋 / ∼ ) ∈ V )
17 10 16 jca ⊢ ( 𝜑 → ( ( 𝐺 ↾s 𝐻 ) ∈ Grp ∧ ( 𝑋 / ∼ ) ∈ V ) )
18 vex ⊢ 𝑦 ∈ V
19 18 mptex ⊢ ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ∈ V
20 19 rnex ⊢ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) ∈ V
21 7 20 fnmpoi ⊢ · Fn ( 𝐻 × ( 𝑋 / ∼ ) )
22 21 a1i ⊢ ( 𝜑 → · Fn ( 𝐻 × ( 𝑋 / ∼ ) ) )
23 eqid ⊢ ( 𝑋 / ∼ ) = ( 𝑋 / ∼ )
24 oveq2 ⊢ ( [ 𝑠 ] ∼ = 𝑣 → ( 𝑢 · [ 𝑠 ] ∼ ) = ( 𝑢 · 𝑣 ) )
25 24 eleq1d ⊢ ( [ 𝑠 ] ∼ = 𝑣 → ( ( 𝑢 · [ 𝑠 ] ∼ ) ∈ ( 𝑋 / ∼ ) ↔ ( 𝑢 · 𝑣 ) ∈ ( 𝑋 / ∼ ) ) )
26 1 2 3 4 5 6 7 sylow2blem1 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐻 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑢 · [ 𝑠 ] ∼ ) = [ ( 𝑢 + 𝑠 ) ] ∼ )
27 6 ovexi ⊢ ∼ ∈ V
28 subgrcl ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
29 3 28 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
30 29 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐻 ∧ 𝑠 ∈ 𝑋 ) → 𝐺 ∈ Grp )
31 1 subgss ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 ⊆ 𝑋 )
32 3 31 syl ⊢ ( 𝜑 → 𝐻 ⊆ 𝑋 )
33 32 sselda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐻 ) → 𝑢 ∈ 𝑋 )
34 33 3adant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐻 ∧ 𝑠 ∈ 𝑋 ) → 𝑢 ∈ 𝑋 )
35 simp3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐻 ∧ 𝑠 ∈ 𝑋 ) → 𝑠 ∈ 𝑋 )
36 1 5 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑢 + 𝑠 ) ∈ 𝑋 )
37 30 34 35 36 syl3anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐻 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑢 + 𝑠 ) ∈ 𝑋 )
38 ecelqsw ⊢ ( ( ∼ ∈ V ∧ ( 𝑢 + 𝑠 ) ∈ 𝑋 ) → [ ( 𝑢 + 𝑠 ) ] ∼ ∈ ( 𝑋 / ∼ ) )
39 27 37 38 sylancr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐻 ∧ 𝑠 ∈ 𝑋 ) → [ ( 𝑢 + 𝑠 ) ] ∼ ∈ ( 𝑋 / ∼ ) )
40 26 39 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐻 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑢 · [ 𝑠 ] ∼ ) ∈ ( 𝑋 / ∼ ) )
41 40 3expa ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝑋 ) → ( 𝑢 · [ 𝑠 ] ∼ ) ∈ ( 𝑋 / ∼ ) )
42 23 25 41 ectocld ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐻 ) ∧ 𝑣 ∈ ( 𝑋 / ∼ ) ) → ( 𝑢 · 𝑣 ) ∈ ( 𝑋 / ∼ ) )
43 42 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐻 ) → ∀ 𝑣 ∈ ( 𝑋 / ∼ ) ( 𝑢 · 𝑣 ) ∈ ( 𝑋 / ∼ ) )
44 43 ralrimiva ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝐻 ∀ 𝑣 ∈ ( 𝑋 / ∼ ) ( 𝑢 · 𝑣 ) ∈ ( 𝑋 / ∼ ) )
45 ffnov ⊢ ( · : ( 𝐻 × ( 𝑋 / ∼ ) ) ⟶ ( 𝑋 / ∼ ) ↔ ( · Fn ( 𝐻 × ( 𝑋 / ∼ ) ) ∧ ∀ 𝑢 ∈ 𝐻 ∀ 𝑣 ∈ ( 𝑋 / ∼ ) ( 𝑢 · 𝑣 ) ∈ ( 𝑋 / ∼ ) ) )
46 22 44 45 sylanbrc ⊢ ( 𝜑 → · : ( 𝐻 × ( 𝑋 / ∼ ) ) ⟶ ( 𝑋 / ∼ ) )
47 8 subgbas ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 = ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) )
48 3 47 syl ⊢ ( 𝜑 → 𝐻 = ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) )
49 48 xpeq1d ⊢ ( 𝜑 → ( 𝐻 × ( 𝑋 / ∼ ) ) = ( ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) × ( 𝑋 / ∼ ) ) )
50 49 feq2d ⊢ ( 𝜑 → ( · : ( 𝐻 × ( 𝑋 / ∼ ) ) ⟶ ( 𝑋 / ∼ ) ↔ · : ( ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) × ( 𝑋 / ∼ ) ) ⟶ ( 𝑋 / ∼ ) ) )
51 46 50 mpbid ⊢ ( 𝜑 → · : ( ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) × ( 𝑋 / ∼ ) ) ⟶ ( 𝑋 / ∼ ) )
52 oveq2 ⊢ ( [ 𝑠 ] ∼ = 𝑢 → ( ( 0g ‘ ( 𝐺 ↾s 𝐻 ) ) · [ 𝑠 ] ∼ ) = ( ( 0g ‘ ( 𝐺 ↾s 𝐻 ) ) · 𝑢 ) )
53 id ⊢ ( [ 𝑠 ] ∼ = 𝑢 → [ 𝑠 ] ∼ = 𝑢 )
54 52 53 eqeq12d ⊢ ( [ 𝑠 ] ∼ = 𝑢 → ( ( ( 0g ‘ ( 𝐺 ↾s 𝐻 ) ) · [ 𝑠 ] ∼ ) = [ 𝑠 ] ∼ ↔ ( ( 0g ‘ ( 𝐺 ↾s 𝐻 ) ) · 𝑢 ) = 𝑢 ) )
55 oveq2 ⊢ ( [ 𝑠 ] ∼ = 𝑢 → ( ( 𝑎 ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) 𝑏 ) · [ 𝑠 ] ∼ ) = ( ( 𝑎 ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) 𝑏 ) · 𝑢 ) )
56 oveq2 ⊢ ( [ 𝑠 ] ∼ = 𝑢 → ( 𝑏 · [ 𝑠 ] ∼ ) = ( 𝑏 · 𝑢 ) )
57 56 oveq2d ⊢ ( [ 𝑠 ] ∼ = 𝑢 → ( 𝑎 · ( 𝑏 · [ 𝑠 ] ∼ ) ) = ( 𝑎 · ( 𝑏 · 𝑢 ) ) )
58 55 57 eqeq12d ⊢ ( [ 𝑠 ] ∼ = 𝑢 → ( ( ( 𝑎 ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) 𝑏 ) · [ 𝑠 ] ∼ ) = ( 𝑎 · ( 𝑏 · [ 𝑠 ] ∼ ) ) ↔ ( ( 𝑎 ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) 𝑏 ) · 𝑢 ) = ( 𝑎 · ( 𝑏 · 𝑢 ) ) ) )
59 58 2ralbidv ⊢ ( [ 𝑠 ] ∼ = 𝑢 → ( ∀ 𝑎 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ∀ 𝑏 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( ( 𝑎 ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) 𝑏 ) · [ 𝑠 ] ∼ ) = ( 𝑎 · ( 𝑏 · [ 𝑠 ] ∼ ) ) ↔ ∀ 𝑎 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ∀ 𝑏 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( ( 𝑎 ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) 𝑏 ) · 𝑢 ) = ( 𝑎 · ( 𝑏 · 𝑢 ) ) ) )
60 54 59 anbi12d ⊢ ( [ 𝑠 ] ∼ = 𝑢 → ( ( ( ( 0g ‘ ( 𝐺 ↾s 𝐻 ) ) · [ 𝑠 ] ∼ ) = [ 𝑠 ] ∼ ∧ ∀ 𝑎 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ∀ 𝑏 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( ( 𝑎 ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) 𝑏 ) · [ 𝑠 ] ∼ ) = ( 𝑎 · ( 𝑏 · [ 𝑠 ] ∼ ) ) ) ↔ ( ( ( 0g ‘ ( 𝐺 ↾s 𝐻 ) ) · 𝑢 ) = 𝑢 ∧ ∀ 𝑎 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ∀ 𝑏 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( ( 𝑎 ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) 𝑏 ) · 𝑢 ) = ( 𝑎 · ( 𝑏 · 𝑢 ) ) ) ) )
61 simpl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → 𝜑 )
62 3 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
63 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
64 63 subg0cl ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝐻 )
65 62 64 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 0g ‘ 𝐺 ) ∈ 𝐻 )
66 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → 𝑠 ∈ 𝑋 )
67 1 2 3 4 5 6 7 sylow2blem1 ⊢ ( ( 𝜑 ∧ ( 0g ‘ 𝐺 ) ∈ 𝐻 ∧ 𝑠 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) · [ 𝑠 ] ∼ ) = [ ( ( 0g ‘ 𝐺 ) + 𝑠 ) ] ∼ )
68 61 65 66 67 syl3anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) · [ 𝑠 ] ∼ ) = [ ( ( 0g ‘ 𝐺 ) + 𝑠 ) ] ∼ )
69 8 63 subg0 ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ ( 𝐺 ↾s 𝐻 ) ) )
70 62 69 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ ( 𝐺 ↾s 𝐻 ) ) )
71 70 oveq1d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) · [ 𝑠 ] ∼ ) = ( ( 0g ‘ ( 𝐺 ↾s 𝐻 ) ) · [ 𝑠 ] ∼ ) )
72 1 5 63 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑠 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) + 𝑠 ) = 𝑠 )
73 29 72 sylan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) + 𝑠 ) = 𝑠 )
74 73 eceq1d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → [ ( ( 0g ‘ 𝐺 ) + 𝑠 ) ] ∼ = [ 𝑠 ] ∼ )
75 68 71 74 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( ( 0g ‘ ( 𝐺 ↾s 𝐻 ) ) · [ 𝑠 ] ∼ ) = [ 𝑠 ] ∼ )
76 62 adantr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
77 76 28 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) → 𝐺 ∈ Grp )
78 76 31 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) → 𝐻 ⊆ 𝑋 )
79 simprl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) → 𝑎 ∈ 𝐻 )
80 78 79 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) → 𝑎 ∈ 𝑋 )
81 simprr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) → 𝑏 ∈ 𝐻 )
82 78 81 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) → 𝑏 ∈ 𝑋 )
83 66 adantr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) → 𝑠 ∈ 𝑋 )
84 1 5 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) ) → ( ( 𝑎 + 𝑏 ) + 𝑠 ) = ( 𝑎 + ( 𝑏 + 𝑠 ) ) )
85 77 80 82 83 84 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) → ( ( 𝑎 + 𝑏 ) + 𝑠 ) = ( 𝑎 + ( 𝑏 + 𝑠 ) ) )
86 85 eceq1d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) → [ ( ( 𝑎 + 𝑏 ) + 𝑠 ) ] ∼ = [ ( 𝑎 + ( 𝑏 + 𝑠 ) ) ] ∼ )
87 61 adantr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) → 𝜑 )
88 1 5 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑏 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑏 + 𝑠 ) ∈ 𝑋 )
89 77 82 83 88 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) → ( 𝑏 + 𝑠 ) ∈ 𝑋 )
90 1 2 3 4 5 6 7 sylow2blem1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ∧ ( 𝑏 + 𝑠 ) ∈ 𝑋 ) → ( 𝑎 · [ ( 𝑏 + 𝑠 ) ] ∼ ) = [ ( 𝑎 + ( 𝑏 + 𝑠 ) ) ] ∼ )
91 87 79 89 90 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) → ( 𝑎 · [ ( 𝑏 + 𝑠 ) ] ∼ ) = [ ( 𝑎 + ( 𝑏 + 𝑠 ) ) ] ∼ )
92 86 91 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) → [ ( ( 𝑎 + 𝑏 ) + 𝑠 ) ] ∼ = ( 𝑎 · [ ( 𝑏 + 𝑠 ) ] ∼ ) )
93 5 subgcl ⊢ ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) → ( 𝑎 + 𝑏 ) ∈ 𝐻 )
94 76 79 81 93 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) → ( 𝑎 + 𝑏 ) ∈ 𝐻 )
95 1 2 3 4 5 6 7 sylow2blem1 ⊢ ( ( 𝜑 ∧ ( 𝑎 + 𝑏 ) ∈ 𝐻 ∧ 𝑠 ∈ 𝑋 ) → ( ( 𝑎 + 𝑏 ) · [ 𝑠 ] ∼ ) = [ ( ( 𝑎 + 𝑏 ) + 𝑠 ) ] ∼ )
96 87 94 83 95 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) → ( ( 𝑎 + 𝑏 ) · [ 𝑠 ] ∼ ) = [ ( ( 𝑎 + 𝑏 ) + 𝑠 ) ] ∼ )
97 1 2 3 4 5 6 7 sylow2blem1 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐻 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑏 · [ 𝑠 ] ∼ ) = [ ( 𝑏 + 𝑠 ) ] ∼ )
98 87 81 83 97 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) → ( 𝑏 · [ 𝑠 ] ∼ ) = [ ( 𝑏 + 𝑠 ) ] ∼ )
99 98 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) → ( 𝑎 · ( 𝑏 · [ 𝑠 ] ∼ ) ) = ( 𝑎 · [ ( 𝑏 + 𝑠 ) ] ∼ ) )
100 92 96 99 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) ) → ( ( 𝑎 + 𝑏 ) · [ 𝑠 ] ∼ ) = ( 𝑎 · ( 𝑏 · [ 𝑠 ] ∼ ) ) )
101 100 ralrimivva ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ∀ 𝑎 ∈ 𝐻 ∀ 𝑏 ∈ 𝐻 ( ( 𝑎 + 𝑏 ) · [ 𝑠 ] ∼ ) = ( 𝑎 · ( 𝑏 · [ 𝑠 ] ∼ ) ) )
102 62 47 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → 𝐻 = ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) )
103 8 5 ressplusg ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → + = ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) )
104 3 103 syl ⊢ ( 𝜑 → + = ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) )
105 104 oveqdr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑎 + 𝑏 ) = ( 𝑎 ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) 𝑏 ) )
106 105 oveq1d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( ( 𝑎 + 𝑏 ) · [ 𝑠 ] ∼ ) = ( ( 𝑎 ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) 𝑏 ) · [ 𝑠 ] ∼ ) )
107 106 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( ( ( 𝑎 + 𝑏 ) · [ 𝑠 ] ∼ ) = ( 𝑎 · ( 𝑏 · [ 𝑠 ] ∼ ) ) ↔ ( ( 𝑎 ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) 𝑏 ) · [ 𝑠 ] ∼ ) = ( 𝑎 · ( 𝑏 · [ 𝑠 ] ∼ ) ) ) )
108 102 107 raleqbidv ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( ∀ 𝑏 ∈ 𝐻 ( ( 𝑎 + 𝑏 ) · [ 𝑠 ] ∼ ) = ( 𝑎 · ( 𝑏 · [ 𝑠 ] ∼ ) ) ↔ ∀ 𝑏 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( ( 𝑎 ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) 𝑏 ) · [ 𝑠 ] ∼ ) = ( 𝑎 · ( 𝑏 · [ 𝑠 ] ∼ ) ) ) )
109 102 108 raleqbidv ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( ∀ 𝑎 ∈ 𝐻 ∀ 𝑏 ∈ 𝐻 ( ( 𝑎 + 𝑏 ) · [ 𝑠 ] ∼ ) = ( 𝑎 · ( 𝑏 · [ 𝑠 ] ∼ ) ) ↔ ∀ 𝑎 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ∀ 𝑏 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( ( 𝑎 ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) 𝑏 ) · [ 𝑠 ] ∼ ) = ( 𝑎 · ( 𝑏 · [ 𝑠 ] ∼ ) ) ) )
110 101 109 mpbid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ∀ 𝑎 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ∀ 𝑏 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( ( 𝑎 ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) 𝑏 ) · [ 𝑠 ] ∼ ) = ( 𝑎 · ( 𝑏 · [ 𝑠 ] ∼ ) ) )
111 75 110 jca ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( ( ( 0g ‘ ( 𝐺 ↾s 𝐻 ) ) · [ 𝑠 ] ∼ ) = [ 𝑠 ] ∼ ∧ ∀ 𝑎 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ∀ 𝑏 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( ( 𝑎 ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) 𝑏 ) · [ 𝑠 ] ∼ ) = ( 𝑎 · ( 𝑏 · [ 𝑠 ] ∼ ) ) ) )
112 23 60 111 ectocld ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑋 / ∼ ) ) → ( ( ( 0g ‘ ( 𝐺 ↾s 𝐻 ) ) · 𝑢 ) = 𝑢 ∧ ∀ 𝑎 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ∀ 𝑏 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( ( 𝑎 ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) 𝑏 ) · 𝑢 ) = ( 𝑎 · ( 𝑏 · 𝑢 ) ) ) )
113 112 ralrimiva ⊢ ( 𝜑 → ∀ 𝑢 ∈ ( 𝑋 / ∼ ) ( ( ( 0g ‘ ( 𝐺 ↾s 𝐻 ) ) · 𝑢 ) = 𝑢 ∧ ∀ 𝑎 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ∀ 𝑏 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( ( 𝑎 ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) 𝑏 ) · 𝑢 ) = ( 𝑎 · ( 𝑏 · 𝑢 ) ) ) )
114 51 113 jca ⊢ ( 𝜑 → ( · : ( ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) × ( 𝑋 / ∼ ) ) ⟶ ( 𝑋 / ∼ ) ∧ ∀ 𝑢 ∈ ( 𝑋 / ∼ ) ( ( ( 0g ‘ ( 𝐺 ↾s 𝐻 ) ) · 𝑢 ) = 𝑢 ∧ ∀ 𝑎 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ∀ 𝑏 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( ( 𝑎 ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) 𝑏 ) · 𝑢 ) = ( 𝑎 · ( 𝑏 · 𝑢 ) ) ) ) )
115 eqid ⊢ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) = ( Base ‘ ( 𝐺 ↾s 𝐻 ) )
116 eqid ⊢ ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) = ( +g ‘ ( 𝐺 ↾s 𝐻 ) )
117 eqid ⊢ ( 0g ‘ ( 𝐺 ↾s 𝐻 ) ) = ( 0g ‘ ( 𝐺 ↾s 𝐻 ) )
118 115 116 117 isga ⊢ ( · ∈ ( ( 𝐺 ↾s 𝐻 ) GrpAct ( 𝑋 / ∼ ) ) ↔ ( ( ( 𝐺 ↾s 𝐻 ) ∈ Grp ∧ ( 𝑋 / ∼ ) ∈ V ) ∧ ( · : ( ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) × ( 𝑋 / ∼ ) ) ⟶ ( 𝑋 / ∼ ) ∧ ∀ 𝑢 ∈ ( 𝑋 / ∼ ) ( ( ( 0g ‘ ( 𝐺 ↾s 𝐻 ) ) · 𝑢 ) = 𝑢 ∧ ∀ 𝑎 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ∀ 𝑏 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( ( 𝑎 ( +g ‘ ( 𝐺 ↾s 𝐻 ) ) 𝑏 ) · 𝑢 ) = ( 𝑎 · ( 𝑏 · 𝑢 ) ) ) ) ) )
119 17 114 118 sylanbrc ⊢ ( 𝜑 → · ∈ ( ( 𝐺 ↾s 𝐻 ) GrpAct ( 𝑋 / ∼ ) ) )