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

Metamath Proof Explorer

Theorem qustgpopn

Description: A quotient map in a topological group is an open map. (Contributed by Mario Carneiro, 18-Sep-2015)

Ref Expression
Hypotheses qustgp.h ⊢ 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑌 ) )
qustgpopn.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
qustgpopn.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
qustgpopn.k ⊢ 𝐾 = ( TopOpen ‘ 𝐻 )
qustgpopn.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) )
Assertion qustgpopn ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → ( 𝐹 “ 𝑆 ) ∈ 𝐾 )

Proof

Step Hyp Ref Expression
1 qustgp.h ⊢ 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑌 ) )
2 qustgpopn.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
3 qustgpopn.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
4 qustgpopn.k ⊢ 𝐾 = ( TopOpen ‘ 𝐻 )
5 qustgpopn.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) )
6 imassrn ⊢ ( 𝐹 “ 𝑆 ) ⊆ ran 𝐹
7 1 a1i ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑌 ) ) )
8 2 a1i ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → 𝑋 = ( Base ‘ 𝐺 ) )
9 ovex ⊢ ( 𝐺 ~QG 𝑌 ) ∈ V
10 9 a1i ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → ( 𝐺 ~QG 𝑌 ) ∈ V )
11 simp1 ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → 𝐺 ∈ TopGrp )
12 7 8 5 10 11 quslem ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → 𝐹 : 𝑋 –onto→ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) )
13 forn ⊢ ( 𝐹 : 𝑋 –onto→ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) → ran 𝐹 = ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) )
14 12 13 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → ran 𝐹 = ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) )
15 6 14 sseqtrid ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → ( 𝐹 “ 𝑆 ) ⊆ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) )
16 eceq1 ⊢ ( 𝑥 = 𝑦 → [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) = [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) )
17 16 cbvmptv ⊢ ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) = ( 𝑦 ∈ 𝑋 ↦ [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) )
18 5 17 eqtri ⊢ 𝐹 = ( 𝑦 ∈ 𝑋 ↦ [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) )
19 18 mptpreima ⊢ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) = { 𝑦 ∈ 𝑋 ∣ [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) ∈ ( 𝐹 “ 𝑆 ) }
20 19 reqabi ⊢ ( 𝑦 ∈ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ↔ ( 𝑦 ∈ 𝑋 ∧ [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) ∈ ( 𝐹 “ 𝑆 ) ) )
21 5 funmpt2 ⊢ Fun 𝐹
22 fvelima ⊢ ( ( Fun 𝐹 ∧ [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) ∈ ( 𝐹 “ 𝑆 ) ) → ∃ 𝑧 ∈ 𝑆 ( 𝐹 ‘ 𝑧 ) = [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) )
23 21 22 mpan ⊢ ( [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) ∈ ( 𝐹 “ 𝑆 ) → ∃ 𝑧 ∈ 𝑆 ( 𝐹 ‘ 𝑧 ) = [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) )
24 3 2 tgptopon ⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
25 11 24 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
26 simp3 ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → 𝑆 ∈ 𝐽 )
27 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐽 ) → 𝑆 ⊆ 𝑋 )
28 25 26 27 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → 𝑆 ⊆ 𝑋 )
29 28 adantr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) → 𝑆 ⊆ 𝑋 )
30 29 sselda ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ∈ 𝑋 )
31 eceq1 ⊢ ( 𝑥 = 𝑧 → [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) = [ 𝑧 ] ( 𝐺 ~QG 𝑌 ) )
32 ecexg ⊢ ( ( 𝐺 ~QG 𝑌 ) ∈ V → [ 𝑧 ] ( 𝐺 ~QG 𝑌 ) ∈ V )
33 9 32 ax-mp ⊢ [ 𝑧 ] ( 𝐺 ~QG 𝑌 ) ∈ V
34 31 5 33 fvmpt ⊢ ( 𝑧 ∈ 𝑋 → ( 𝐹 ‘ 𝑧 ) = [ 𝑧 ] ( 𝐺 ~QG 𝑌 ) )
35 30 34 syl ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝐹 ‘ 𝑧 ) = [ 𝑧 ] ( 𝐺 ~QG 𝑌 ) )
36 35 eqeq1d ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑧 ) = [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) ↔ [ 𝑧 ] ( 𝐺 ~QG 𝑌 ) = [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) ) )
37 eqcom ⊢ ( [ 𝑧 ] ( 𝐺 ~QG 𝑌 ) = [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) ↔ [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) = [ 𝑧 ] ( 𝐺 ~QG 𝑌 ) )
38 36 37 bitrdi ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑧 ) = [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) ↔ [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) = [ 𝑧 ] ( 𝐺 ~QG 𝑌 ) ) )
39 nsgsubg ⊢ ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑌 ∈ ( SubGrp ‘ 𝐺 ) )
40 39 3ad2ant2 ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → 𝑌 ∈ ( SubGrp ‘ 𝐺 ) )
41 40 ad2antrr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) → 𝑌 ∈ ( SubGrp ‘ 𝐺 ) )
42 eqid ⊢ ( 𝐺 ~QG 𝑌 ) = ( 𝐺 ~QG 𝑌 )
43 2 42 eqger ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ~QG 𝑌 ) Er 𝑋 )
44 41 43 syl ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝐺 ~QG 𝑌 ) Er 𝑋 )
45 simplr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) → 𝑦 ∈ 𝑋 )
46 44 45 erth ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑦 ( 𝐺 ~QG 𝑌 ) 𝑧 ↔ [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) = [ 𝑧 ] ( 𝐺 ~QG 𝑌 ) ) )
47 11 ad2antrr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) → 𝐺 ∈ TopGrp )
48 2 subgss ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝑌 ⊆ 𝑋 )
49 41 48 syl ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) → 𝑌 ⊆ 𝑋 )
50 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
51 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
52 2 50 51 42 eqgval ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑦 ( 𝐺 ~QG 𝑌 ) 𝑧 ↔ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ) )
53 47 49 52 syl2anc ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑦 ( 𝐺 ~QG 𝑌 ) 𝑧 ↔ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ) )
54 38 46 53 3bitr2d ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑧 ) = [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) ↔ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ) )
55 eqid ⊢ ( oppg ‘ 𝐺 ) = ( oppg ‘ 𝐺 )
56 eqid ⊢ ( +g ‘ ( oppg ‘ 𝐺 ) ) = ( +g ‘ ( oppg ‘ 𝐺 ) )
57 51 55 56 oppgplus ⊢ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑎 ) = ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) )
58 57 mpteq2i ⊢ ( 𝑎 ∈ 𝑋 ↦ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑎 ) ) = ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) )
59 47 adantr ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → 𝐺 ∈ TopGrp )
60 55 oppgtgp ⊢ ( 𝐺 ∈ TopGrp → ( oppg ‘ 𝐺 ) ∈ TopGrp )
61 59 60 syl ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → ( oppg ‘ 𝐺 ) ∈ TopGrp )
62 49 sselda ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑋 )
63 eqid ⊢ ( 𝑎 ∈ 𝑋 ↦ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑎 ) ) = ( 𝑎 ∈ 𝑋 ↦ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑎 ) )
64 55 2 oppgbas ⊢ 𝑋 = ( Base ‘ ( oppg ‘ 𝐺 ) )
65 55 3 oppgtopn ⊢ 𝐽 = ( TopOpen ‘ ( oppg ‘ 𝐺 ) )
66 63 64 56 65 tgplacthmeo ⊢ ( ( ( oppg ‘ 𝐺 ) ∈ TopGrp ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑋 ) → ( 𝑎 ∈ 𝑋 ↦ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑎 ) ) ∈ ( 𝐽 Homeo 𝐽 ) )
67 61 62 66 syl2anc ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → ( 𝑎 ∈ 𝑋 ↦ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑎 ) ) ∈ ( 𝐽 Homeo 𝐽 ) )
68 58 67 eqeltrrid ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) ∈ ( 𝐽 Homeo 𝐽 ) )
69 hmeocn ⊢ ( ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) ∈ ( 𝐽 Homeo 𝐽 ) → ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) )
70 68 69 syl ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) )
71 26 ad3antrrr ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → 𝑆 ∈ 𝐽 )
72 cnima ⊢ ( ( ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑆 ∈ 𝐽 ) → ( ◡ ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) “ 𝑆 ) ∈ 𝐽 )
73 70 71 72 syl2anc ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → ( ◡ ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) “ 𝑆 ) ∈ 𝐽 )
74 45 adantr ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → 𝑦 ∈ 𝑋 )
75 tgpgrp ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )
76 59 75 syl ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → 𝐺 ∈ Grp )
77 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
78 2 51 77 50 grprinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋 ) → ( 𝑦 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) = ( 0g ‘ 𝐺 ) )
79 76 74 78 syl2anc ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → ( 𝑦 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) = ( 0g ‘ 𝐺 ) )
80 79 oveq1d ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → ( ( 𝑦 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ( +g ‘ 𝐺 ) 𝑧 ) = ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑧 ) )
81 2 50 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑋 )
82 76 74 81 syl2anc ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑋 )
83 30 adantr ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → 𝑧 ∈ 𝑋 )
84 2 51 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑦 ∈ 𝑋 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑦 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑦 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) )
85 76 74 82 83 84 syl13anc ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → ( ( 𝑦 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑦 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) )
86 2 51 77 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑧 ) = 𝑧 )
87 76 83 86 syl2anc ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑧 ) = 𝑧 )
88 80 85 87 3eqtr3d ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → ( 𝑦 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) = 𝑧 )
89 simplr ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → 𝑧 ∈ 𝑆 )
90 88 89 eqeltrd ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → ( 𝑦 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ 𝑆 )
91 oveq1 ⊢ ( 𝑎 = 𝑦 → ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) = ( 𝑦 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) )
92 91 eleq1d ⊢ ( 𝑎 = 𝑦 → ( ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ 𝑆 ↔ ( 𝑦 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ 𝑆 ) )
93 eqid ⊢ ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) = ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) )
94 93 mptpreima ⊢ ( ◡ ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) “ 𝑆 ) = { 𝑎 ∈ 𝑋 ∣ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ 𝑆 }
95 92 94 elrab2 ⊢ ( 𝑦 ∈ ( ◡ ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) “ 𝑆 ) ↔ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ 𝑆 ) )
96 74 90 95 sylanbrc ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → 𝑦 ∈ ( ◡ ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) “ 𝑆 ) )
97 ecexg ⊢ ( ( 𝐺 ~QG 𝑌 ) ∈ V → [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ∈ V )
98 9 97 ax-mp ⊢ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ∈ V
99 98 5 fnmpti ⊢ 𝐹 Fn 𝑋
100 29 ad3antrrr ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → 𝑆 ⊆ 𝑋 )
101 fnfvima ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ 𝑆 ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) ∈ ( 𝐹 “ 𝑆 ) )
102 101 3expia ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ 𝑆 → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) ∈ ( 𝐹 “ 𝑆 ) ) )
103 99 100 102 sylancr ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → ( ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ 𝑆 → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) ∈ ( 𝐹 “ 𝑆 ) ) )
104 76 adantr ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → 𝐺 ∈ Grp )
105 simpr ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → 𝑎 ∈ 𝑋 )
106 62 adantr ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑋 )
107 2 51 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑎 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑋 ) → ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ 𝑋 )
108 104 105 106 107 syl3anc ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ 𝑋 )
109 eceq1 ⊢ ( 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) → [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) = [ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ] ( 𝐺 ~QG 𝑌 ) )
110 109 5 98 fvmpt3i ⊢ ( ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ 𝑋 → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) = [ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ] ( 𝐺 ~QG 𝑌 ) )
111 108 110 syl ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) = [ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ] ( 𝐺 ~QG 𝑌 ) )
112 44 ad2antrr ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → ( 𝐺 ~QG 𝑌 ) Er 𝑋 )
113 2 51 77 50 grplinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑎 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) 𝑎 ) = ( 0g ‘ 𝐺 ) )
114 104 105 113 syl2anc ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) 𝑎 ) = ( 0g ‘ 𝐺 ) )
115 114 oveq1d ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) = ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) )
116 2 50 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑎 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑋 )
117 104 105 116 syl2anc ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑋 )
118 2 51 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑋 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) )
119 104 117 105 106 118 syl13anc ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) )
120 2 51 77 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) )
121 104 106 120 syl2anc ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) )
122 115 119 121 3eqtr3d ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) )
123 simplr ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 )
124 122 123 eqeltrd ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) ∈ 𝑌 )
125 49 ad2antrr ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → 𝑌 ⊆ 𝑋 )
126 2 50 51 42 eqgval ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑎 ( 𝐺 ~QG 𝑌 ) ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ↔ ( 𝑎 ∈ 𝑋 ∧ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) ∈ 𝑌 ) ) )
127 104 125 126 syl2anc ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → ( 𝑎 ( 𝐺 ~QG 𝑌 ) ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ↔ ( 𝑎 ∈ 𝑋 ∧ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) ∈ 𝑌 ) ) )
128 105 108 124 127 mpbir3and ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → 𝑎 ( 𝐺 ~QG 𝑌 ) ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) )
129 112 128 erthi ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) = [ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ] ( 𝐺 ~QG 𝑌 ) )
130 111 129 eqtr4d ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) = [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) )
131 130 eleq1d ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → ( ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) ∈ ( 𝐹 “ 𝑆 ) ↔ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) ∈ ( 𝐹 “ 𝑆 ) ) )
132 103 131 sylibd ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) → ( ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ 𝑆 → [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) ∈ ( 𝐹 “ 𝑆 ) ) )
133 132 ss2rabdv ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → { 𝑎 ∈ 𝑋 ∣ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ 𝑆 } ⊆ { 𝑎 ∈ 𝑋 ∣ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) ∈ ( 𝐹 “ 𝑆 ) } )
134 eceq1 ⊢ ( 𝑥 = 𝑎 → [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) = [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) )
135 134 cbvmptv ⊢ ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) = ( 𝑎 ∈ 𝑋 ↦ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) )
136 5 135 eqtri ⊢ 𝐹 = ( 𝑎 ∈ 𝑋 ↦ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) )
137 136 mptpreima ⊢ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) = { 𝑎 ∈ 𝑋 ∣ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) ∈ ( 𝐹 “ 𝑆 ) }
138 133 94 137 3sstr4g ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → ( ◡ ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) “ 𝑆 ) ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) )
139 eleq2 ⊢ ( 𝑢 = ( ◡ ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) “ 𝑆 ) → ( 𝑦 ∈ 𝑢 ↔ 𝑦 ∈ ( ◡ ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) “ 𝑆 ) ) )
140 sseq1 ⊢ ( 𝑢 = ( ◡ ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) “ 𝑆 ) → ( 𝑢 ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ↔ ( ◡ ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) “ 𝑆 ) ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ) )
141 139 140 anbi12d ⊢ ( 𝑢 = ( ◡ ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) “ 𝑆 ) → ( ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ) ↔ ( 𝑦 ∈ ( ◡ ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) “ 𝑆 ) ∧ ( ◡ ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) “ 𝑆 ) ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ) ) )
142 141 rspcev ⊢ ( ( ( ◡ ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) “ 𝑆 ) ∈ 𝐽 ∧ ( 𝑦 ∈ ( ◡ ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) “ 𝑆 ) ∧ ( ◡ ( 𝑎 ∈ 𝑋 ↦ ( 𝑎 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ) ) “ 𝑆 ) ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ) )
143 73 96 138 142 syl12anc ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ) )
144 143 3ad2antr3 ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ) )
145 144 ex ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑌 ) → ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ) ) )
146 54 145 sylbid ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑧 ) = [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) → ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ) ) )
147 146 rexlimdva ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) → ( ∃ 𝑧 ∈ 𝑆 ( 𝐹 ‘ 𝑧 ) = [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) → ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ) ) )
148 23 147 syl5 ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑋 ) → ( [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) ∈ ( 𝐹 “ 𝑆 ) → ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ) ) )
149 148 expimpd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → ( ( 𝑦 ∈ 𝑋 ∧ [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) ∈ ( 𝐹 “ 𝑆 ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ) ) )
150 20 149 biimtrid ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → ( 𝑦 ∈ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ) ) )
151 150 ralrimiv ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → ∀ 𝑦 ∈ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ) )
152 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
153 eltop2 ⊢ ( 𝐽 ∈ Top → ( ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ∈ 𝐽 ↔ ∀ 𝑦 ∈ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ) ) )
154 25 152 153 3syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → ( ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ∈ 𝐽 ↔ ∀ 𝑦 ∈ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ) ) )
155 151 154 mpbird ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ∈ 𝐽 )
156 elqtop3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ) → ( ( 𝐹 “ 𝑆 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ( 𝐹 “ 𝑆 ) ⊆ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ∧ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ∈ 𝐽 ) ) )
157 25 12 156 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → ( ( 𝐹 “ 𝑆 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ( 𝐹 “ 𝑆 ) ⊆ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ∧ ( ◡ 𝐹 “ ( 𝐹 “ 𝑆 ) ) ∈ 𝐽 ) ) )
158 15 155 157 mpbir2and ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → ( 𝐹 “ 𝑆 ) ∈ ( 𝐽 qTop 𝐹 ) )
159 7 8 5 10 11 qusval ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → 𝐻 = ( 𝐹 “s 𝐺 ) )
160 159 8 12 11 3 4 imastopn ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → 𝐾 = ( 𝐽 qTop 𝐹 ) )
161 158 160 eleqtrrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → ( 𝐹 “ 𝑆 ) ∈ 𝐾 )