Metamath Proof Explorer

Theorem sylow2blem3

Description: Sylow's second theorem. Putting together the results of sylow2a and the orbit-stabilizer theorem to show that P does not divide the set of all fixed points under the group action, we get that there is a fixed point of the group action, so that there is some g e. X with h g K = g K for all h e. H . This implies that invg ( g ) h g e. K , so h is in the conjugated subgroup g K invg ( g ) . (Contributed by Mario Carneiro, 18-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 ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) )
sylow2blem3.hp ⊢ ( 𝜑 → 𝑃 pGrp ( 𝐺 ↾s 𝐻 ) )
sylow2blem3.kn ⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) )
sylow2blem3.d ⊢ − = ( -g ‘ 𝐺 )
Assertion sylow2blem3 ( 𝜑 → ∃ 𝑔 ∈ 𝑋 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) )

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 sylow2blem3.hp ⊢ ( 𝜑 → 𝑃 pGrp ( 𝐺 ↾s 𝐻 ) )
9 sylow2blem3.kn ⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) )
10 sylow2blem3.d ⊢ − = ( -g ‘ 𝐺 )
11 pgpprm ⊢ ( 𝑃 pGrp ( 𝐺 ↾s 𝐻 ) → 𝑃 ∈ ℙ )
12 8 11 syl ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
13 subgrcl ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
14 3 13 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
15 1 grpbn0 ⊢ ( 𝐺 ∈ Grp → 𝑋 ≠ ∅ )
16 14 15 syl ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
17 hashnncl ⊢ ( 𝑋 ∈ Fin → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
18 2 17 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
19 16 18 mpbird ⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℕ )
20 pcndvds2 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ♯ ‘ 𝑋 ) ∈ ℕ ) → ¬ 𝑃 ∥ ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )
21 12 19 20 syl2anc ⊢ ( 𝜑 → ¬ 𝑃 ∥ ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )
22 1 6 4 2 lagsubg2 ⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) = ( ( ♯ ‘ ( 𝑋 / ∼ ) ) · ( ♯ ‘ 𝐾 ) ) )
23 22 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) / ( ♯ ‘ 𝐾 ) ) = ( ( ( ♯ ‘ ( 𝑋 / ∼ ) ) · ( ♯ ‘ 𝐾 ) ) / ( ♯ ‘ 𝐾 ) ) )
24 9 oveq2d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) / ( ♯ ‘ 𝐾 ) ) = ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )
25 pwfi ⊢ ( 𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin )
26 2 25 sylib ⊢ ( 𝜑 → 𝒫 𝑋 ∈ Fin )
27 1 6 eqger ⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → ∼ Er 𝑋 )
28 4 27 syl ⊢ ( 𝜑 → ∼ Er 𝑋 )
29 28 qsss ⊢ ( 𝜑 → ( 𝑋 / ∼ ) ⊆ 𝒫 𝑋 )
30 26 29 ssfid ⊢ ( 𝜑 → ( 𝑋 / ∼ ) ∈ Fin )
31 hashcl ⊢ ( ( 𝑋 / ∼ ) ∈ Fin → ( ♯ ‘ ( 𝑋 / ∼ ) ) ∈ ℕ0 )
32 30 31 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑋 / ∼ ) ) ∈ ℕ0 )
33 32 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑋 / ∼ ) ) ∈ ℂ )
34 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
35 34 subg0cl ⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝐾 )
36 4 35 syl ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ 𝐾 )
37 36 ne0d ⊢ ( 𝜑 → 𝐾 ≠ ∅ )
38 1 subgss ⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → 𝐾 ⊆ 𝑋 )
39 4 38 syl ⊢ ( 𝜑 → 𝐾 ⊆ 𝑋 )
40 2 39 ssfid ⊢ ( 𝜑 → 𝐾 ∈ Fin )
41 hashnncl ⊢ ( 𝐾 ∈ Fin → ( ( ♯ ‘ 𝐾 ) ∈ ℕ ↔ 𝐾 ≠ ∅ ) )
42 40 41 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐾 ) ∈ ℕ ↔ 𝐾 ≠ ∅ ) )
43 37 42 mpbird ⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ∈ ℕ )
44 43 nncnd ⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ∈ ℂ )
45 43 nnne0d ⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ≠ 0 )
46 33 44 45 divcan4d ⊢ ( 𝜑 → ( ( ( ♯ ‘ ( 𝑋 / ∼ ) ) · ( ♯ ‘ 𝐾 ) ) / ( ♯ ‘ 𝐾 ) ) = ( ♯ ‘ ( 𝑋 / ∼ ) ) )
47 23 24 46 3eqtr3d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) = ( ♯ ‘ ( 𝑋 / ∼ ) ) )
48 47 breq2d ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ↔ 𝑃 ∥ ( ♯ ‘ ( 𝑋 / ∼ ) ) ) )
49 21 48 mtbid ⊢ ( 𝜑 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝑋 / ∼ ) ) )
50 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
51 12 50 syl ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
52 32 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑋 / ∼ ) ) ∈ ℤ )
53 ssrab2 ⊢ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ⊆ ( 𝑋 / ∼ )
54 ssfi ⊢ ( ( ( 𝑋 / ∼ ) ∈ Fin ∧ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ⊆ ( 𝑋 / ∼ ) ) → { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ∈ Fin )
55 30 53 54 sylancl ⊢ ( 𝜑 → { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ∈ Fin )
56 hashcl ⊢ ( { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ∈ Fin → ( ♯ ‘ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ) ∈ ℕ0 )
57 55 56 syl ⊢ ( 𝜑 → ( ♯ ‘ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ) ∈ ℕ0 )
58 57 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ) ∈ ℤ )
59 eqid ⊢ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) = ( Base ‘ ( 𝐺 ↾s 𝐻 ) )
60 1 2 3 4 5 6 7 sylow2blem2 ⊢ ( 𝜑 → · ∈ ( ( 𝐺 ↾s 𝐻 ) GrpAct ( 𝑋 / ∼ ) ) )
61 eqid ⊢ ( 𝐺 ↾s 𝐻 ) = ( 𝐺 ↾s 𝐻 )
62 61 subgbas ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 = ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) )
63 3 62 syl ⊢ ( 𝜑 → 𝐻 = ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) )
64 1 subgss ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 ⊆ 𝑋 )
65 3 64 syl ⊢ ( 𝜑 → 𝐻 ⊆ 𝑋 )
66 2 65 ssfid ⊢ ( 𝜑 → 𝐻 ∈ Fin )
67 63 66 eqeltrrd ⊢ ( 𝜑 → ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ∈ Fin )
68 eqid ⊢ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } = { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 }
69 eqid ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑋 / ∼ ) ∧ ∃ 𝑔 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑔 · 𝑥 ) = 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( 𝑋 / ∼ ) ∧ ∃ 𝑔 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑔 · 𝑥 ) = 𝑦 ) }
70 59 60 8 67 30 68 69 sylow2a ⊢ ( 𝜑 → 𝑃 ∥ ( ( ♯ ‘ ( 𝑋 / ∼ ) ) − ( ♯ ‘ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ) ) )
71 dvdssub2 ⊢ ( ( ( 𝑃 ∈ ℤ ∧ ( ♯ ‘ ( 𝑋 / ∼ ) ) ∈ ℤ ∧ ( ♯ ‘ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ) ∈ ℤ ) ∧ 𝑃 ∥ ( ( ♯ ‘ ( 𝑋 / ∼ ) ) − ( ♯ ‘ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ) ) ) → ( 𝑃 ∥ ( ♯ ‘ ( 𝑋 / ∼ ) ) ↔ 𝑃 ∥ ( ♯ ‘ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ) ) )
72 51 52 58 70 71 syl31anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( ♯ ‘ ( 𝑋 / ∼ ) ) ↔ 𝑃 ∥ ( ♯ ‘ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ) ) )
73 49 72 mtbid ⊢ ( 𝜑 → ¬ 𝑃 ∥ ( ♯ ‘ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ) )
74 hasheq0 ⊢ ( { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ∈ Fin → ( ( ♯ ‘ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ) = 0 ↔ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } = ∅ ) )
75 55 74 syl ⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ) = 0 ↔ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } = ∅ ) )
76 dvds0 ⊢ ( 𝑃 ∈ ℤ → 𝑃 ∥ 0 )
77 51 76 syl ⊢ ( 𝜑 → 𝑃 ∥ 0 )
78 breq2 ⊢ ( ( ♯ ‘ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ) = 0 → ( 𝑃 ∥ ( ♯ ‘ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ) ↔ 𝑃 ∥ 0 ) )
79 77 78 syl5ibrcom ⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ) = 0 → 𝑃 ∥ ( ♯ ‘ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ) ) )
80 75 79 sylbird ⊢ ( 𝜑 → ( { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } = ∅ → 𝑃 ∥ ( ♯ ‘ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ) ) )
81 80 necon3bd ⊢ ( 𝜑 → ( ¬ 𝑃 ∥ ( ♯ ‘ { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ) → { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ≠ ∅ ) )
82 73 81 mpd ⊢ ( 𝜑 → { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ≠ ∅ )
83 rabn0 ⊢ ( { 𝑧 ∈ ( 𝑋 / ∼ ) ∣ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 } ≠ ∅ ↔ ∃ 𝑧 ∈ ( 𝑋 / ∼ ) ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 )
84 82 83 sylib ⊢ ( 𝜑 → ∃ 𝑧 ∈ ( 𝑋 / ∼ ) ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 )
85 63 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑢 ∈ 𝐻 ( 𝑢 · 𝑧 ) = 𝑧 ↔ ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 ) )
86 85 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( 𝑋 / ∼ ) ∀ 𝑢 ∈ 𝐻 ( 𝑢 · 𝑧 ) = 𝑧 ↔ ∃ 𝑧 ∈ ( 𝑋 / ∼ ) ∀ 𝑢 ∈ ( Base ‘ ( 𝐺 ↾s 𝐻 ) ) ( 𝑢 · 𝑧 ) = 𝑧 ) )
87 84 86 mpbird ⊢ ( 𝜑 → ∃ 𝑧 ∈ ( 𝑋 / ∼ ) ∀ 𝑢 ∈ 𝐻 ( 𝑢 · 𝑧 ) = 𝑧 )
88 vex ⊢ 𝑧 ∈ V
89 88 elqs ⊢ ( 𝑧 ∈ ( 𝑋 / ∼ ) ↔ ∃ 𝑔 ∈ 𝑋 𝑧 = [ 𝑔 ] ∼ )
90 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → 𝑧 = [ 𝑔 ] ∼ )
91 90 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → ( 𝑢 · 𝑧 ) = ( 𝑢 · [ 𝑔 ] ∼ ) )
92 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → ( 𝑢 · 𝑧 ) = 𝑧 )
93 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → 𝜑 )
94 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → 𝑢 ∈ 𝐻 )
95 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → 𝑔 ∈ 𝑋 )
96 1 2 3 4 5 6 7 sylow2blem1 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐻 ∧ 𝑔 ∈ 𝑋 ) → ( 𝑢 · [ 𝑔 ] ∼ ) = [ ( 𝑢 + 𝑔 ) ] ∼ )
97 93 94 95 96 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → ( 𝑢 · [ 𝑔 ] ∼ ) = [ ( 𝑢 + 𝑔 ) ] ∼ )
98 91 92 97 3eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → 𝑧 = [ ( 𝑢 + 𝑔 ) ] ∼ )
99 90 98 eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → [ 𝑔 ] ∼ = [ ( 𝑢 + 𝑔 ) ] ∼ )
100 28 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → ∼ Er 𝑋 )
101 100 95 erth ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → ( 𝑔 ∼ ( 𝑢 + 𝑔 ) ↔ [ 𝑔 ] ∼ = [ ( 𝑢 + 𝑔 ) ] ∼ ) )
102 99 101 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → 𝑔 ∼ ( 𝑢 + 𝑔 ) )
103 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → 𝐺 ∈ Grp )
104 39 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → 𝐾 ⊆ 𝑋 )
105 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
106 1 105 5 6 eqgval ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐾 ⊆ 𝑋 ) → ( 𝑔 ∼ ( 𝑢 + 𝑔 ) ↔ ( 𝑔 ∈ 𝑋 ∧ ( 𝑢 + 𝑔 ) ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) ∈ 𝐾 ) ) )
107 103 104 106 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → ( 𝑔 ∼ ( 𝑢 + 𝑔 ) ↔ ( 𝑔 ∈ 𝑋 ∧ ( 𝑢 + 𝑔 ) ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) ∈ 𝐾 ) ) )
108 102 107 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → ( 𝑔 ∈ 𝑋 ∧ ( 𝑢 + 𝑔 ) ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) ∈ 𝐾 ) )
109 108 simp3d ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) ∈ 𝐾 )
110 oveq2 ⊢ ( 𝑥 = ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) → ( 𝑔 + 𝑥 ) = ( 𝑔 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) ) )
111 110 oveq1d ⊢ ( 𝑥 = ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) → ( ( 𝑔 + 𝑥 ) − 𝑔 ) = ( ( 𝑔 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) ) − 𝑔 ) )
112 eqid ⊢ ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) = ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) )
113 ovex ⊢ ( ( 𝑔 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) ) − 𝑔 ) ∈ V
114 111 112 113 fvmpt ⊢ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) ∈ 𝐾 → ( ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) ) = ( ( 𝑔 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) ) − 𝑔 ) )
115 109 114 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → ( ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) ) = ( ( 𝑔 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) ) − 𝑔 ) )
116 1 5 34 105 grprinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑔 ∈ 𝑋 ) → ( 𝑔 + ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) ) = ( 0g ‘ 𝐺 ) )
117 103 95 116 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → ( 𝑔 + ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) ) = ( 0g ‘ 𝐺 ) )
118 117 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → ( ( 𝑔 + ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) ) + ( 𝑢 + 𝑔 ) ) = ( ( 0g ‘ 𝐺 ) + ( 𝑢 + 𝑔 ) ) )
119 1 105 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑔 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) ∈ 𝑋 )
120 103 95 119 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) ∈ 𝑋 )
121 65 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → 𝐻 ⊆ 𝑋 )
122 121 94 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → 𝑢 ∈ 𝑋 )
123 1 5 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( 𝑢 + 𝑔 ) ∈ 𝑋 )
124 103 122 95 123 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → ( 𝑢 + 𝑔 ) ∈ 𝑋 )
125 1 5 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑔 ∈ 𝑋 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) ∈ 𝑋 ∧ ( 𝑢 + 𝑔 ) ∈ 𝑋 ) ) → ( ( 𝑔 + ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) ) + ( 𝑢 + 𝑔 ) ) = ( 𝑔 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) ) )
126 103 95 120 124 125 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → ( ( 𝑔 + ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) ) + ( 𝑢 + 𝑔 ) ) = ( 𝑔 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) ) )
127 1 5 34 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑢 + 𝑔 ) ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) + ( 𝑢 + 𝑔 ) ) = ( 𝑢 + 𝑔 ) )
128 103 124 127 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → ( ( 0g ‘ 𝐺 ) + ( 𝑢 + 𝑔 ) ) = ( 𝑢 + 𝑔 ) )
129 118 126 128 3eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → ( 𝑔 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) ) = ( 𝑢 + 𝑔 ) )
130 129 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → ( ( 𝑔 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) ) − 𝑔 ) = ( ( 𝑢 + 𝑔 ) − 𝑔 ) )
131 1 5 10 grppncan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( ( 𝑢 + 𝑔 ) − 𝑔 ) = 𝑢 )
132 103 122 95 131 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → ( ( 𝑢 + 𝑔 ) − 𝑔 ) = 𝑢 )
133 115 130 132 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → ( ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) ) = 𝑢 )
134 ovex ⊢ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ∈ V
135 134 112 fnmpti ⊢ ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) Fn 𝐾
136 fnfvelrn ⊢ ( ( ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) Fn 𝐾 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) ∈ 𝐾 ) → ( ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) ) ∈ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) )
137 135 109 136 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → ( ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) + ( 𝑢 + 𝑔 ) ) ) ∈ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) )
138 133 137 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ( 𝑢 ∈ 𝐻 ∧ ( 𝑢 · 𝑧 ) = 𝑧 ) ) → 𝑢 ∈ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) )
139 138 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ 𝑢 ∈ 𝐻 ) → ( ( 𝑢 · 𝑧 ) = 𝑧 → 𝑢 ∈ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ) )
140 139 ralimdva ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) → ( ∀ 𝑢 ∈ 𝐻 ( 𝑢 · 𝑧 ) = 𝑧 → ∀ 𝑢 ∈ 𝐻 𝑢 ∈ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ) )
141 140 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) ∧ ∀ 𝑢 ∈ 𝐻 ( 𝑢 · 𝑧 ) = 𝑧 ) → ∀ 𝑢 ∈ 𝐻 𝑢 ∈ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) )
142 141 an32s ⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ 𝐻 ( 𝑢 · 𝑧 ) = 𝑧 ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) → ∀ 𝑢 ∈ 𝐻 𝑢 ∈ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) )
143 dfss3 ⊢ ( 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ↔ ∀ 𝑢 ∈ 𝐻 𝑢 ∈ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) )
144 142 143 sylibr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ 𝐻 ( 𝑢 · 𝑧 ) = 𝑧 ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝑧 = [ 𝑔 ] ∼ ) ) → 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) )
145 144 expr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ 𝐻 ( 𝑢 · 𝑧 ) = 𝑧 ) ∧ 𝑔 ∈ 𝑋 ) → ( 𝑧 = [ 𝑔 ] ∼ → 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ) )
146 145 reximdva ⊢ ( ( 𝜑 ∧ ∀ 𝑢 ∈ 𝐻 ( 𝑢 · 𝑧 ) = 𝑧 ) → ( ∃ 𝑔 ∈ 𝑋 𝑧 = [ 𝑔 ] ∼ → ∃ 𝑔 ∈ 𝑋 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ) )
147 146 ex ⊢ ( 𝜑 → ( ∀ 𝑢 ∈ 𝐻 ( 𝑢 · 𝑧 ) = 𝑧 → ( ∃ 𝑔 ∈ 𝑋 𝑧 = [ 𝑔 ] ∼ → ∃ 𝑔 ∈ 𝑋 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ) ) )
148 147 com23 ⊢ ( 𝜑 → ( ∃ 𝑔 ∈ 𝑋 𝑧 = [ 𝑔 ] ∼ → ( ∀ 𝑢 ∈ 𝐻 ( 𝑢 · 𝑧 ) = 𝑧 → ∃ 𝑔 ∈ 𝑋 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ) ) )
149 89 148 syl5bi ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑋 / ∼ ) → ( ∀ 𝑢 ∈ 𝐻 ( 𝑢 · 𝑧 ) = 𝑧 → ∃ 𝑔 ∈ 𝑋 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ) ) )
150 149 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( 𝑋 / ∼ ) ∀ 𝑢 ∈ 𝐻 ( 𝑢 · 𝑧 ) = 𝑧 → ∃ 𝑔 ∈ 𝑋 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) ) )
151 87 150 mpd ⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝑋 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) )