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

Metamath Proof Explorer

Theorem qustgplem

Description: Lemma for qustgp . (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 𝑌 ) )
qustgplem.m ⊢ − = ( 𝑧 ∈ 𝑋 , 𝑤 ∈ 𝑋 ↦ [ ( 𝑧 ( -g ‘ 𝐺 ) 𝑤 ) ] ( 𝐺 ~QG 𝑌 ) )
Assertion qustgplem ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝐻 ∈ TopGrp )

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 qustgplem.m ⊢ − = ( 𝑧 ∈ 𝑋 , 𝑤 ∈ 𝑋 ↦ [ ( 𝑧 ( -g ‘ 𝐺 ) 𝑤 ) ] ( 𝐺 ~QG 𝑌 ) )
7 1 qusgrp ⊢ ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐻 ∈ Grp )
8 7 adantl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝐻 ∈ Grp )
9 1 a1i ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑌 ) ) )
10 2 a1i ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝑋 = ( Base ‘ 𝐺 ) )
11 ovex ⊢ ( 𝐺 ~QG 𝑌 ) ∈ V
12 11 a1i ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( 𝐺 ~QG 𝑌 ) ∈ V )
13 simpl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝐺 ∈ TopGrp )
14 9 10 5 12 13 qusval ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝐻 = ( 𝐹 “s 𝐺 ) )
15 9 10 5 12 13 quslem ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝐹 : 𝑋 –onto→ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) )
16 14 10 15 13 3 4 imastopn ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝐾 = ( 𝐽 qTop 𝐹 ) )
17 3 2 tgptopon ⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
18 17 adantr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
19 qtoptopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ) → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ) )
20 18 15 19 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ) )
21 16 20 eqeltrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝐾 ∈ ( TopOn ‘ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ) )
22 9 10 12 13 qusbas ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) = ( Base ‘ 𝐻 ) )
23 22 fveq2d ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( TopOn ‘ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ) = ( TopOn ‘ ( Base ‘ 𝐻 ) ) )
24 21 23 eleqtrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝐻 ) ) )
25 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
26 25 4 istps ⊢ ( 𝐻 ∈ TopSp ↔ 𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝐻 ) ) )
27 24 26 sylibr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝐻 ∈ TopSp )
28 eqid ⊢ ( -g ‘ 𝐻 ) = ( -g ‘ 𝐻 )
29 25 28 grpsubf ⊢ ( 𝐻 ∈ Grp → ( -g ‘ 𝐻 ) : ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) ⟶ ( Base ‘ 𝐻 ) )
30 8 29 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( -g ‘ 𝐻 ) : ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) ⟶ ( Base ‘ 𝐻 ) )
31 cnvimass ⊢ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ⊆ dom ( -g ‘ 𝐻 )
32 30 fdmd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → dom ( -g ‘ 𝐻 ) = ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) )
33 32 adantr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) → dom ( -g ‘ 𝐻 ) = ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) )
34 31 33 sseqtrid ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) → ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ⊆ ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) )
35 relxp ⊢ Rel ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) )
36 relss ⊢ ( ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ⊆ ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) → ( Rel ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) → Rel ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) )
37 34 35 36 mpisyl ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) → Rel ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) )
38 34 sseld ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) ) )
39 vex ⊢ 𝑥 ∈ V
40 39 elqs ⊢ ( 𝑥 ∈ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ↔ ∃ 𝑎 ∈ 𝑋 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) )
41 22 adantr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) → ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) = ( Base ‘ 𝐻 ) )
42 41 eleq2d ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) → ( 𝑥 ∈ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ↔ 𝑥 ∈ ( Base ‘ 𝐻 ) ) )
43 40 42 bitr3id ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) → ( ∃ 𝑎 ∈ 𝑋 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) ↔ 𝑥 ∈ ( Base ‘ 𝐻 ) ) )
44 vex ⊢ 𝑦 ∈ V
45 44 elqs ⊢ ( 𝑦 ∈ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ↔ ∃ 𝑏 ∈ 𝑋 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) )
46 41 eleq2d ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) → ( 𝑦 ∈ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ↔ 𝑦 ∈ ( Base ‘ 𝐻 ) ) )
47 45 46 bitr3id ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) → ( ∃ 𝑏 ∈ 𝑋 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ↔ 𝑦 ∈ ( Base ‘ 𝐻 ) ) )
48 43 47 anbi12d ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) → ( ( ∃ 𝑎 ∈ 𝑋 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) ∧ ∃ 𝑏 ∈ 𝑋 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) )
49 reeanv ⊢ ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) ∧ 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ) ↔ ( ∃ 𝑎 ∈ 𝑋 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) ∧ ∃ 𝑏 ∈ 𝑋 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ) )
50 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) )
51 48 49 50 3bitr4g ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) → ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) ∧ 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) ) )
52 8 ad2antrr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 𝐻 ∈ Grp )
53 52 29 syl ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( -g ‘ 𝐻 ) : ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) ⟶ ( Base ‘ 𝐻 ) )
54 ffn ⊢ ( ( -g ‘ 𝐻 ) : ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) ⟶ ( Base ‘ 𝐻 ) → ( -g ‘ 𝐻 ) Fn ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) )
55 elpreima ⊢ ( ( -g ‘ 𝐻 ) Fn ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) → ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ↔ ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) ∧ ( ( -g ‘ 𝐻 ) ‘ ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ) ∈ 𝑢 ) ) )
56 53 54 55 3syl ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ↔ ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) ∧ ( ( -g ‘ 𝐻 ) ‘ ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ) ∈ 𝑢 ) ) )
57 df-ov ⊢ ( [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) ( -g ‘ 𝐻 ) [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ) = ( ( -g ‘ 𝐻 ) ‘ ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ )
58 simpllr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) )
59 simprl ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 𝑎 ∈ 𝑋 )
60 simprr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 𝑏 ∈ 𝑋 )
61 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
62 1 2 61 28 qussub ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) ( -g ‘ 𝐻 ) [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ) = [ ( 𝑎 ( -g ‘ 𝐺 ) 𝑏 ) ] ( 𝐺 ~QG 𝑌 ) )
63 58 59 60 62 syl3anc ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) ( -g ‘ 𝐻 ) [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ) = [ ( 𝑎 ( -g ‘ 𝐺 ) 𝑏 ) ] ( 𝐺 ~QG 𝑌 ) )
64 57 63 eqtr3id ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( -g ‘ 𝐻 ) ‘ ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ) = [ ( 𝑎 ( -g ‘ 𝐺 ) 𝑏 ) ] ( 𝐺 ~QG 𝑌 ) )
65 64 eleq1d ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( ( -g ‘ 𝐻 ) ‘ ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ) ∈ 𝑢 ↔ [ ( 𝑎 ( -g ‘ 𝐺 ) 𝑏 ) ] ( 𝐺 ~QG 𝑌 ) ∈ 𝑢 ) )
66 simpr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) )
67 tgpgrp ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )
68 67 adantr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝐺 ∈ Grp )
69 2 61 grpsubf ⊢ ( 𝐺 ∈ Grp → ( -g ‘ 𝐺 ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
70 ffn ⊢ ( ( -g ‘ 𝐺 ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 → ( -g ‘ 𝐺 ) Fn ( 𝑋 × 𝑋 ) )
71 68 69 70 3syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( -g ‘ 𝐺 ) Fn ( 𝑋 × 𝑋 ) )
72 fnov ⊢ ( ( -g ‘ 𝐺 ) Fn ( 𝑋 × 𝑋 ) ↔ ( -g ‘ 𝐺 ) = ( 𝑧 ∈ 𝑋 , 𝑤 ∈ 𝑋 ↦ ( 𝑧 ( -g ‘ 𝐺 ) 𝑤 ) ) )
73 71 72 sylib ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( -g ‘ 𝐺 ) = ( 𝑧 ∈ 𝑋 , 𝑤 ∈ 𝑋 ↦ ( 𝑧 ( -g ‘ 𝐺 ) 𝑤 ) ) )
74 3 61 tgpsubcn ⊢ ( 𝐺 ∈ TopGrp → ( -g ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
75 74 adantr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( -g ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
76 73 75 eqeltrrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( 𝑧 ∈ 𝑋 , 𝑤 ∈ 𝑋 ↦ ( 𝑧 ( -g ‘ 𝐺 ) 𝑤 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
77 ecexg ⊢ ( ( 𝐺 ~QG 𝑌 ) ∈ V → [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ∈ V )
78 11 77 ax-mp ⊢ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ∈ V
79 78 5 fnmpti ⊢ 𝐹 Fn 𝑋
80 qtopid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) )
81 18 79 80 sylancl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) )
82 16 oveq2d ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( 𝐽 Cn 𝐾 ) = ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) )
83 81 82 eleqtrrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
84 5 83 eqeltrrid ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
85 eceq1 ⊢ ( 𝑥 = ( 𝑧 ( -g ‘ 𝐺 ) 𝑤 ) → [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) = [ ( 𝑧 ( -g ‘ 𝐺 ) 𝑤 ) ] ( 𝐺 ~QG 𝑌 ) )
86 18 18 76 18 84 85 cnmpt21 ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( 𝑧 ∈ 𝑋 , 𝑤 ∈ 𝑋 ↦ [ ( 𝑧 ( -g ‘ 𝐺 ) 𝑤 ) ] ( 𝐺 ~QG 𝑌 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
87 6 86 eqeltrid ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → − ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
88 87 ad2antrr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → − ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
89 simplr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 𝑢 ∈ 𝐾 )
90 cnima ⊢ ( ( − ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) ∧ 𝑢 ∈ 𝐾 ) → ( ◡ − “ 𝑢 ) ∈ ( 𝐽 ×t 𝐽 ) )
91 88 89 90 syl2anc ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ◡ − “ 𝑢 ) ∈ ( 𝐽 ×t 𝐽 ) )
92 18 ad2antrr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
93 eltx ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( ( ◡ − “ 𝑢 ) ∈ ( 𝐽 ×t 𝐽 ) ↔ ∀ 𝑡 ∈ ( ◡ − “ 𝑢 ) ∃ 𝑐 ∈ 𝐽 ∃ 𝑑 ∈ 𝐽 ( 𝑡 ∈ ( 𝑐 × 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) )
94 92 92 93 syl2anc ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( ◡ − “ 𝑢 ) ∈ ( 𝐽 ×t 𝐽 ) ↔ ∀ 𝑡 ∈ ( ◡ − “ 𝑢 ) ∃ 𝑐 ∈ 𝐽 ∃ 𝑑 ∈ 𝐽 ( 𝑡 ∈ ( 𝑐 × 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) )
95 91 94 mpbid ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ∀ 𝑡 ∈ ( ◡ − “ 𝑢 ) ∃ 𝑐 ∈ 𝐽 ∃ 𝑑 ∈ 𝐽 ( 𝑡 ∈ ( 𝑐 × 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) )
96 ecexg ⊢ ( ( 𝐺 ~QG 𝑌 ) ∈ V → [ ( 𝑧 ( -g ‘ 𝐺 ) 𝑤 ) ] ( 𝐺 ~QG 𝑌 ) ∈ V )
97 11 96 ax-mp ⊢ [ ( 𝑧 ( -g ‘ 𝐺 ) 𝑤 ) ] ( 𝐺 ~QG 𝑌 ) ∈ V
98 6 97 fnmpoi ⊢ − Fn ( 𝑋 × 𝑋 )
99 elpreima ⊢ ( − Fn ( 𝑋 × 𝑋 ) → ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( ◡ − “ 𝑢 ) ↔ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑋 × 𝑋 ) ∧ ( − ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ∈ 𝑢 ) ) )
100 98 99 ax-mp ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( ◡ − “ 𝑢 ) ↔ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑋 × 𝑋 ) ∧ ( − ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ∈ 𝑢 ) )
101 opelxp ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑋 × 𝑋 ) ↔ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) )
102 101 anbi1i ⊢ ( ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑋 × 𝑋 ) ∧ ( − ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ∈ 𝑢 ) ↔ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ ( − ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ∈ 𝑢 ) )
103 df-ov ⊢ ( 𝑎 − 𝑏 ) = ( − ‘ ⟨ 𝑎 , 𝑏 ⟩ )
104 oveq12 ⊢ ( ( 𝑧 = 𝑎 ∧ 𝑤 = 𝑏 ) → ( 𝑧 ( -g ‘ 𝐺 ) 𝑤 ) = ( 𝑎 ( -g ‘ 𝐺 ) 𝑏 ) )
105 104 eceq1d ⊢ ( ( 𝑧 = 𝑎 ∧ 𝑤 = 𝑏 ) → [ ( 𝑧 ( -g ‘ 𝐺 ) 𝑤 ) ] ( 𝐺 ~QG 𝑌 ) = [ ( 𝑎 ( -g ‘ 𝐺 ) 𝑏 ) ] ( 𝐺 ~QG 𝑌 ) )
106 ecexg ⊢ ( ( 𝐺 ~QG 𝑌 ) ∈ V → [ ( 𝑎 ( -g ‘ 𝐺 ) 𝑏 ) ] ( 𝐺 ~QG 𝑌 ) ∈ V )
107 11 106 ax-mp ⊢ [ ( 𝑎 ( -g ‘ 𝐺 ) 𝑏 ) ] ( 𝐺 ~QG 𝑌 ) ∈ V
108 105 6 107 ovmpoa ⊢ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( 𝑎 − 𝑏 ) = [ ( 𝑎 ( -g ‘ 𝐺 ) 𝑏 ) ] ( 𝐺 ~QG 𝑌 ) )
109 103 108 eqtr3id ⊢ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( − ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = [ ( 𝑎 ( -g ‘ 𝐺 ) 𝑏 ) ] ( 𝐺 ~QG 𝑌 ) )
110 109 eleq1d ⊢ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( ( − ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ∈ 𝑢 ↔ [ ( 𝑎 ( -g ‘ 𝐺 ) 𝑏 ) ] ( 𝐺 ~QG 𝑌 ) ∈ 𝑢 ) )
111 110 pm5.32i ⊢ ( ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ ( − ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ∈ 𝑢 ) ↔ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ [ ( 𝑎 ( -g ‘ 𝐺 ) 𝑏 ) ] ( 𝐺 ~QG 𝑌 ) ∈ 𝑢 ) )
112 100 102 111 3bitri ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( ◡ − “ 𝑢 ) ↔ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ [ ( 𝑎 ( -g ‘ 𝐺 ) 𝑏 ) ] ( 𝐺 ~QG 𝑌 ) ∈ 𝑢 ) )
113 eleq1 ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑡 ∈ ( 𝑐 × 𝑑 ) ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑐 × 𝑑 ) ) )
114 opelxp ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑐 × 𝑑 ) ↔ ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) )
115 113 114 bitrdi ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑡 ∈ ( 𝑐 × 𝑑 ) ↔ ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ) )
116 115 anbi1d ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑡 ∈ ( 𝑐 × 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ↔ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) )
117 116 2rexbidv ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ → ( ∃ 𝑐 ∈ 𝐽 ∃ 𝑑 ∈ 𝐽 ( 𝑡 ∈ ( 𝑐 × 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ↔ ∃ 𝑐 ∈ 𝐽 ∃ 𝑑 ∈ 𝐽 ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) )
118 117 rspccv ⊢ ( ∀ 𝑡 ∈ ( ◡ − “ 𝑢 ) ∃ 𝑐 ∈ 𝐽 ∃ 𝑑 ∈ 𝐽 ( 𝑡 ∈ ( 𝑐 × 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( ◡ − “ 𝑢 ) → ∃ 𝑐 ∈ 𝐽 ∃ 𝑑 ∈ 𝐽 ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) )
119 112 118 biimtrrid ⊢ ( ∀ 𝑡 ∈ ( ◡ − “ 𝑢 ) ∃ 𝑐 ∈ 𝐽 ∃ 𝑑 ∈ 𝐽 ( 𝑡 ∈ ( 𝑐 × 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) → ( ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ [ ( 𝑎 ( -g ‘ 𝐺 ) 𝑏 ) ] ( 𝐺 ~QG 𝑌 ) ∈ 𝑢 ) → ∃ 𝑐 ∈ 𝐽 ∃ 𝑑 ∈ 𝐽 ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) )
120 95 119 syl ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ [ ( 𝑎 ( -g ‘ 𝐺 ) 𝑏 ) ] ( 𝐺 ~QG 𝑌 ) ∈ 𝑢 ) → ∃ 𝑐 ∈ 𝐽 ∃ 𝑑 ∈ 𝐽 ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) )
121 66 120 mpand ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( [ ( 𝑎 ( -g ‘ 𝐺 ) 𝑏 ) ] ( 𝐺 ~QG 𝑌 ) ∈ 𝑢 → ∃ 𝑐 ∈ 𝐽 ∃ 𝑑 ∈ 𝐽 ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) )
122 simp-4l ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → 𝐺 ∈ TopGrp )
123 58 adantr ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) )
124 simprll ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → 𝑐 ∈ 𝐽 )
125 1 2 3 4 5 qustgpopn ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑐 ∈ 𝐽 ) → ( 𝐹 “ 𝑐 ) ∈ 𝐾 )
126 122 123 124 125 syl3anc ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → ( 𝐹 “ 𝑐 ) ∈ 𝐾 )
127 simprlr ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → 𝑑 ∈ 𝐽 )
128 1 2 3 4 5 qustgpopn ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑑 ∈ 𝐽 ) → ( 𝐹 “ 𝑑 ) ∈ 𝐾 )
129 122 123 127 128 syl3anc ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → ( 𝐹 “ 𝑑 ) ∈ 𝐾 )
130 59 adantr ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → 𝑎 ∈ 𝑋 )
131 eceq1 ⊢ ( 𝑥 = 𝑎 → [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) = [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) )
132 131 5 78 fvmpt3i ⊢ ( 𝑎 ∈ 𝑋 → ( 𝐹 ‘ 𝑎 ) = [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) )
133 130 132 syl ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → ( 𝐹 ‘ 𝑎 ) = [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) )
134 122 17 syl ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
135 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑐 ∈ 𝐽 ) → 𝑐 ⊆ 𝑋 )
136 134 124 135 syl2anc ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → 𝑐 ⊆ 𝑋 )
137 simprrl ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) )
138 137 simpld ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → 𝑎 ∈ 𝑐 )
139 fnfvima ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑐 ⊆ 𝑋 ∧ 𝑎 ∈ 𝑐 ) → ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝑐 ) )
140 79 136 138 139 mp3an2i ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝑐 ) )
141 133 140 eqeltrrd ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) ∈ ( 𝐹 “ 𝑐 ) )
142 60 adantr ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → 𝑏 ∈ 𝑋 )
143 eceq1 ⊢ ( 𝑥 = 𝑏 → [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) = [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) )
144 143 5 78 fvmpt3i ⊢ ( 𝑏 ∈ 𝑋 → ( 𝐹 ‘ 𝑏 ) = [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) )
145 142 144 syl ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → ( 𝐹 ‘ 𝑏 ) = [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) )
146 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑑 ∈ 𝐽 ) → 𝑑 ⊆ 𝑋 )
147 134 127 146 syl2anc ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → 𝑑 ⊆ 𝑋 )
148 137 simprd ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → 𝑏 ∈ 𝑑 )
149 fnfvima ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑑 ⊆ 𝑋 ∧ 𝑏 ∈ 𝑑 ) → ( 𝐹 ‘ 𝑏 ) ∈ ( 𝐹 “ 𝑑 ) )
150 79 147 148 149 mp3an2i ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → ( 𝐹 ‘ 𝑏 ) ∈ ( 𝐹 “ 𝑑 ) )
151 145 150 eqeltrrd ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ∈ ( 𝐹 “ 𝑑 ) )
152 141 151 opelxpd ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ( 𝐹 “ 𝑐 ) × ( 𝐹 “ 𝑑 ) ) )
153 136 sselda ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) ∧ 𝑝 ∈ 𝑐 ) → 𝑝 ∈ 𝑋 )
154 147 sselda ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) ∧ 𝑞 ∈ 𝑑 ) → 𝑞 ∈ 𝑋 )
155 153 154 anim12dan ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) ∧ ( 𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑 ) ) → ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) )
156 eceq1 ⊢ ( 𝑥 = 𝑝 → [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) = [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) )
157 156 5 78 fvmpt3i ⊢ ( 𝑝 ∈ 𝑋 → ( 𝐹 ‘ 𝑝 ) = [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) )
158 eceq1 ⊢ ( 𝑥 = 𝑞 → [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) = [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) )
159 158 5 78 fvmpt3i ⊢ ( 𝑞 ∈ 𝑋 → ( 𝐹 ‘ 𝑞 ) = [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) )
160 opeq12 ⊢ ( ( ( 𝐹 ‘ 𝑝 ) = [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) ∧ ( 𝐹 ‘ 𝑞 ) = [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ) → ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ = ⟨ [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ⟩ )
161 157 159 160 syl2an ⊢ ( ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) → ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ = ⟨ [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ⟩ )
162 155 161 syl ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) ∧ ( 𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑 ) ) → ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ = ⟨ [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ⟩ )
163 123 adantr ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) ∧ ( 𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑 ) ) → 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) )
164 1 2 25 quseccl ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑝 ∈ 𝑋 ) → [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) ∈ ( Base ‘ 𝐻 ) )
165 1 2 25 quseccl ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑞 ∈ 𝑋 ) → [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ∈ ( Base ‘ 𝐻 ) )
166 164 165 anim12dan ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) → ( [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) ∈ ( Base ‘ 𝐻 ) ∧ [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ∈ ( Base ‘ 𝐻 ) ) )
167 163 155 166 syl2anc ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) ∧ ( 𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑 ) ) → ( [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) ∈ ( Base ‘ 𝐻 ) ∧ [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ∈ ( Base ‘ 𝐻 ) ) )
168 opelxpi ⊢ ( ( [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) ∈ ( Base ‘ 𝐻 ) ∧ [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ∈ ( Base ‘ 𝐻 ) ) → ⟨ [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) )
169 167 168 syl ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) ∧ ( 𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑 ) ) → ⟨ [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) )
170 1 2 61 28 qussub ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) → ( [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) ( -g ‘ 𝐻 ) [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ) = [ ( 𝑝 ( -g ‘ 𝐺 ) 𝑞 ) ] ( 𝐺 ~QG 𝑌 ) )
171 170 3expb ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) → ( [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) ( -g ‘ 𝐻 ) [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ) = [ ( 𝑝 ( -g ‘ 𝐺 ) 𝑞 ) ] ( 𝐺 ~QG 𝑌 ) )
172 163 155 171 syl2anc ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) ∧ ( 𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑 ) ) → ( [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) ( -g ‘ 𝐻 ) [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ) = [ ( 𝑝 ( -g ‘ 𝐺 ) 𝑞 ) ] ( 𝐺 ~QG 𝑌 ) )
173 oveq12 ⊢ ( ( 𝑧 = 𝑝 ∧ 𝑤 = 𝑞 ) → ( 𝑧 ( -g ‘ 𝐺 ) 𝑤 ) = ( 𝑝 ( -g ‘ 𝐺 ) 𝑞 ) )
174 173 eceq1d ⊢ ( ( 𝑧 = 𝑝 ∧ 𝑤 = 𝑞 ) → [ ( 𝑧 ( -g ‘ 𝐺 ) 𝑤 ) ] ( 𝐺 ~QG 𝑌 ) = [ ( 𝑝 ( -g ‘ 𝐺 ) 𝑞 ) ] ( 𝐺 ~QG 𝑌 ) )
175 ecexg ⊢ ( ( 𝐺 ~QG 𝑌 ) ∈ V → [ ( 𝑝 ( -g ‘ 𝐺 ) 𝑞 ) ] ( 𝐺 ~QG 𝑌 ) ∈ V )
176 11 175 ax-mp ⊢ [ ( 𝑝 ( -g ‘ 𝐺 ) 𝑞 ) ] ( 𝐺 ~QG 𝑌 ) ∈ V
177 174 6 176 ovmpoa ⊢ ( ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) → ( 𝑝 − 𝑞 ) = [ ( 𝑝 ( -g ‘ 𝐺 ) 𝑞 ) ] ( 𝐺 ~QG 𝑌 ) )
178 155 177 syl ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) ∧ ( 𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑 ) ) → ( 𝑝 − 𝑞 ) = [ ( 𝑝 ( -g ‘ 𝐺 ) 𝑞 ) ] ( 𝐺 ~QG 𝑌 ) )
179 172 178 eqtr4d ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) ∧ ( 𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑 ) ) → ( [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) ( -g ‘ 𝐻 ) [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ) = ( 𝑝 − 𝑞 ) )
180 df-ov ⊢ ( [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) ( -g ‘ 𝐻 ) [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ) = ( ( -g ‘ 𝐻 ) ‘ ⟨ [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ⟩ )
181 df-ov ⊢ ( 𝑝 − 𝑞 ) = ( − ‘ ⟨ 𝑝 , 𝑞 ⟩ )
182 179 180 181 3eqtr3g ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) ∧ ( 𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑 ) ) → ( ( -g ‘ 𝐻 ) ‘ ⟨ [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ⟩ ) = ( − ‘ ⟨ 𝑝 , 𝑞 ⟩ ) )
183 opelxpi ⊢ ( ( 𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑 ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ ( 𝑐 × 𝑑 ) )
184 simprrr ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) )
185 184 sselda ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( 𝑐 × 𝑑 ) ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ◡ − “ 𝑢 ) )
186 183 185 sylan2 ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) ∧ ( 𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑 ) ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ◡ − “ 𝑢 ) )
187 elpreima ⊢ ( − Fn ( 𝑋 × 𝑋 ) → ( ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ◡ − “ 𝑢 ) ↔ ( ⟨ 𝑝 , 𝑞 ⟩ ∈ ( 𝑋 × 𝑋 ) ∧ ( − ‘ ⟨ 𝑝 , 𝑞 ⟩ ) ∈ 𝑢 ) ) )
188 98 187 ax-mp ⊢ ( ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ◡ − “ 𝑢 ) ↔ ( ⟨ 𝑝 , 𝑞 ⟩ ∈ ( 𝑋 × 𝑋 ) ∧ ( − ‘ ⟨ 𝑝 , 𝑞 ⟩ ) ∈ 𝑢 ) )
189 188 simprbi ⊢ ( ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ◡ − “ 𝑢 ) → ( − ‘ ⟨ 𝑝 , 𝑞 ⟩ ) ∈ 𝑢 )
190 186 189 syl ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) ∧ ( 𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑 ) ) → ( − ‘ ⟨ 𝑝 , 𝑞 ⟩ ) ∈ 𝑢 )
191 182 190 eqeltrd ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) ∧ ( 𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑 ) ) → ( ( -g ‘ 𝐻 ) ‘ ⟨ [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ⟩ ) ∈ 𝑢 )
192 53 54 syl ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( -g ‘ 𝐻 ) Fn ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) )
193 192 ad2antrr ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) ∧ ( 𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑 ) ) → ( -g ‘ 𝐻 ) Fn ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) )
194 elpreima ⊢ ( ( -g ‘ 𝐻 ) Fn ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) → ( ⟨ [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ↔ ( ⟨ [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) ∧ ( ( -g ‘ 𝐻 ) ‘ ⟨ [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ⟩ ) ∈ 𝑢 ) ) )
195 193 194 syl ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) ∧ ( 𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑 ) ) → ( ⟨ [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ↔ ( ⟨ [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) ∧ ( ( -g ‘ 𝐻 ) ‘ ⟨ [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ⟩ ) ∈ 𝑢 ) ) )
196 169 191 195 mpbir2and ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) ∧ ( 𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑 ) ) → ⟨ [ 𝑝 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑞 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) )
197 162 196 eqeltrd ⊢ ( ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) ∧ ( 𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑 ) ) → ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) )
198 197 ralrimivva ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → ∀ 𝑝 ∈ 𝑐 ∀ 𝑞 ∈ 𝑑 ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) )
199 opeq1 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑝 ) → ⟨ 𝑧 , 𝑤 ⟩ = ⟨ ( 𝐹 ‘ 𝑝 ) , 𝑤 ⟩ )
200 199 eleq1d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑝 ) → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ↔ ⟨ ( 𝐹 ‘ 𝑝 ) , 𝑤 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) )
201 200 ralbidv ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑝 ) → ( ∀ 𝑤 ∈ ( 𝐹 “ 𝑑 ) ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ↔ ∀ 𝑤 ∈ ( 𝐹 “ 𝑑 ) ⟨ ( 𝐹 ‘ 𝑝 ) , 𝑤 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) )
202 201 ralima ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑐 ⊆ 𝑋 ) → ( ∀ 𝑧 ∈ ( 𝐹 “ 𝑐 ) ∀ 𝑤 ∈ ( 𝐹 “ 𝑑 ) ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ↔ ∀ 𝑝 ∈ 𝑐 ∀ 𝑤 ∈ ( 𝐹 “ 𝑑 ) ⟨ ( 𝐹 ‘ 𝑝 ) , 𝑤 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) )
203 79 202 mpan ⊢ ( 𝑐 ⊆ 𝑋 → ( ∀ 𝑧 ∈ ( 𝐹 “ 𝑐 ) ∀ 𝑤 ∈ ( 𝐹 “ 𝑑 ) ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ↔ ∀ 𝑝 ∈ 𝑐 ∀ 𝑤 ∈ ( 𝐹 “ 𝑑 ) ⟨ ( 𝐹 ‘ 𝑝 ) , 𝑤 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) )
204 opeq2 ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑞 ) → ⟨ ( 𝐹 ‘ 𝑝 ) , 𝑤 ⟩ = ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ )
205 204 eleq1d ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑞 ) → ( ⟨ ( 𝐹 ‘ 𝑝 ) , 𝑤 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ↔ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) )
206 205 ralima ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑑 ⊆ 𝑋 ) → ( ∀ 𝑤 ∈ ( 𝐹 “ 𝑑 ) ⟨ ( 𝐹 ‘ 𝑝 ) , 𝑤 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ↔ ∀ 𝑞 ∈ 𝑑 ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) )
207 79 206 mpan ⊢ ( 𝑑 ⊆ 𝑋 → ( ∀ 𝑤 ∈ ( 𝐹 “ 𝑑 ) ⟨ ( 𝐹 ‘ 𝑝 ) , 𝑤 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ↔ ∀ 𝑞 ∈ 𝑑 ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) )
208 207 ralbidv ⊢ ( 𝑑 ⊆ 𝑋 → ( ∀ 𝑝 ∈ 𝑐 ∀ 𝑤 ∈ ( 𝐹 “ 𝑑 ) ⟨ ( 𝐹 ‘ 𝑝 ) , 𝑤 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ↔ ∀ 𝑝 ∈ 𝑐 ∀ 𝑞 ∈ 𝑑 ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) )
209 203 208 sylan9bb ⊢ ( ( 𝑐 ⊆ 𝑋 ∧ 𝑑 ⊆ 𝑋 ) → ( ∀ 𝑧 ∈ ( 𝐹 “ 𝑐 ) ∀ 𝑤 ∈ ( 𝐹 “ 𝑑 ) ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ↔ ∀ 𝑝 ∈ 𝑐 ∀ 𝑞 ∈ 𝑑 ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) )
210 136 147 209 syl2anc ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → ( ∀ 𝑧 ∈ ( 𝐹 “ 𝑐 ) ∀ 𝑤 ∈ ( 𝐹 “ 𝑑 ) ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ↔ ∀ 𝑝 ∈ 𝑐 ∀ 𝑞 ∈ 𝑑 ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) )
211 198 210 mpbird ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → ∀ 𝑧 ∈ ( 𝐹 “ 𝑐 ) ∀ 𝑤 ∈ ( 𝐹 “ 𝑑 ) ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) )
212 dfss3 ⊢ ( ( ( 𝐹 “ 𝑐 ) × ( 𝐹 “ 𝑑 ) ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ↔ ∀ 𝑦 ∈ ( ( 𝐹 “ 𝑐 ) × ( 𝐹 “ 𝑑 ) ) 𝑦 ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) )
213 eleq1 ⊢ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝑦 ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) )
214 213 ralxp ⊢ ( ∀ 𝑦 ∈ ( ( 𝐹 “ 𝑐 ) × ( 𝐹 “ 𝑑 ) ) 𝑦 ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ↔ ∀ 𝑧 ∈ ( 𝐹 “ 𝑐 ) ∀ 𝑤 ∈ ( 𝐹 “ 𝑑 ) ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) )
215 212 214 bitri ⊢ ( ( ( 𝐹 “ 𝑐 ) × ( 𝐹 “ 𝑑 ) ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ↔ ∀ 𝑧 ∈ ( 𝐹 “ 𝑐 ) ∀ 𝑤 ∈ ( 𝐹 “ 𝑑 ) ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) )
216 211 215 sylibr ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → ( ( 𝐹 “ 𝑐 ) × ( 𝐹 “ 𝑑 ) ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) )
217 xpeq1 ⊢ ( 𝑟 = ( 𝐹 “ 𝑐 ) → ( 𝑟 × 𝑠 ) = ( ( 𝐹 “ 𝑐 ) × 𝑠 ) )
218 217 eleq2d ⊢ ( 𝑟 = ( 𝐹 “ 𝑐 ) → ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( 𝑟 × 𝑠 ) ↔ ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ( 𝐹 “ 𝑐 ) × 𝑠 ) ) )
219 217 sseq1d ⊢ ( 𝑟 = ( 𝐹 “ 𝑐 ) → ( ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ↔ ( ( 𝐹 “ 𝑐 ) × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) )
220 218 219 anbi12d ⊢ ( 𝑟 = ( 𝐹 “ 𝑐 ) → ( ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) ↔ ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ( 𝐹 “ 𝑐 ) × 𝑠 ) ∧ ( ( 𝐹 “ 𝑐 ) × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) ) )
221 xpeq2 ⊢ ( 𝑠 = ( 𝐹 “ 𝑑 ) → ( ( 𝐹 “ 𝑐 ) × 𝑠 ) = ( ( 𝐹 “ 𝑐 ) × ( 𝐹 “ 𝑑 ) ) )
222 221 eleq2d ⊢ ( 𝑠 = ( 𝐹 “ 𝑑 ) → ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ( 𝐹 “ 𝑐 ) × 𝑠 ) ↔ ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ( 𝐹 “ 𝑐 ) × ( 𝐹 “ 𝑑 ) ) ) )
223 221 sseq1d ⊢ ( 𝑠 = ( 𝐹 “ 𝑑 ) → ( ( ( 𝐹 “ 𝑐 ) × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ↔ ( ( 𝐹 “ 𝑐 ) × ( 𝐹 “ 𝑑 ) ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) )
224 222 223 anbi12d ⊢ ( 𝑠 = ( 𝐹 “ 𝑑 ) → ( ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ( 𝐹 “ 𝑐 ) × 𝑠 ) ∧ ( ( 𝐹 “ 𝑐 ) × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) ↔ ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ( 𝐹 “ 𝑐 ) × ( 𝐹 “ 𝑑 ) ) ∧ ( ( 𝐹 “ 𝑐 ) × ( 𝐹 “ 𝑑 ) ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) ) )
225 220 224 rspc2ev ⊢ ( ( ( 𝐹 “ 𝑐 ) ∈ 𝐾 ∧ ( 𝐹 “ 𝑑 ) ∈ 𝐾 ∧ ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ( 𝐹 “ 𝑐 ) × ( 𝐹 “ 𝑑 ) ) ∧ ( ( 𝐹 “ 𝑐 ) × ( 𝐹 “ 𝑑 ) ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) ) → ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) )
226 126 129 152 216 225 syl112anc ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ∧ ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) ) ) → ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) )
227 226 expr ⊢ ( ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ) → ( ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) → ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) ) )
228 227 rexlimdvva ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ∃ 𝑐 ∈ 𝐽 ∃ 𝑑 ∈ 𝐽 ( ( 𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( ◡ − “ 𝑢 ) ) → ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) ) )
229 121 228 syld ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( [ ( 𝑎 ( -g ‘ 𝐺 ) 𝑏 ) ] ( 𝐺 ~QG 𝑌 ) ∈ 𝑢 → ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) ) )
230 65 229 sylbid ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( ( -g ‘ 𝐻 ) ‘ ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ) ∈ 𝑢 → ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) ) )
231 230 adantld ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) ∧ ( ( -g ‘ 𝐻 ) ‘ ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ) ∈ 𝑢 ) → ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) ) )
232 56 231 sylbid ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) → ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) ) )
233 opeq12 ⊢ ( ( 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) ∧ 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ )
234 233 eleq1d ⊢ ( ( 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) ∧ 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ↔ ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) )
235 233 eleq1d ⊢ ( ( 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) ∧ 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { 𝑤 ∣ ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) } ↔ ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ { 𝑤 ∣ ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) } ) )
236 opex ⊢ ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ V
237 eleq1 ⊢ ( 𝑤 = ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ → ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ↔ ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( 𝑟 × 𝑠 ) ) )
238 237 anbi1d ⊢ ( 𝑤 = ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ → ( ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) ↔ ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) ) )
239 238 2rexbidv ⊢ ( 𝑤 = ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ → ( ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) ↔ ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) ) )
240 236 239 elab ⊢ ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ { 𝑤 ∣ ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) } ↔ ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) )
241 235 240 bitrdi ⊢ ( ( 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) ∧ 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { 𝑤 ∣ ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) } ↔ ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) ) )
242 234 241 imbi12d ⊢ ( ( 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) ∧ 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ { 𝑤 ∣ ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) } ) ↔ ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) → ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( ⟨ [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) , [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) ) ) )
243 232 242 syl5ibrcom ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) ∧ 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ { 𝑤 ∣ ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) } ) ) )
244 243 rexlimdvva ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) → ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑌 ) ∧ 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑌 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ { 𝑤 ∣ ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) } ) ) )
245 51 244 sylbird ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ { 𝑤 ∣ ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) } ) ) )
246 245 com23 ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ { 𝑤 ∣ ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) } ) ) )
247 38 246 mpdd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ { 𝑤 ∣ ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) } ) )
248 37 247 relssdv ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) → ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ⊆ { 𝑤 ∣ ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) } )
249 ssabral ⊢ ( ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ⊆ { 𝑤 ∣ ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) } ↔ ∀ 𝑤 ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) )
250 248 249 sylib ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) → ∀ 𝑤 ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) )
251 eltx ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝐻 ) ) ∧ 𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝐻 ) ) ) → ( ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ∈ ( 𝐾 ×t 𝐾 ) ↔ ∀ 𝑤 ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) ) )
252 24 24 251 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ∈ ( 𝐾 ×t 𝐾 ) ↔ ∀ 𝑤 ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) ) )
253 252 adantr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) → ( ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ∈ ( 𝐾 ×t 𝐾 ) ↔ ∀ 𝑤 ∈ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ∃ 𝑟 ∈ 𝐾 ∃ 𝑠 ∈ 𝐾 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ) ) )
254 250 253 mpbird ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐾 ) → ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ∈ ( 𝐾 ×t 𝐾 ) )
255 254 ralrimiva ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ∀ 𝑢 ∈ 𝐾 ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ∈ ( 𝐾 ×t 𝐾 ) )
256 txtopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝐻 ) ) ∧ 𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝐻 ) ) ) → ( 𝐾 ×t 𝐾 ) ∈ ( TopOn ‘ ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) ) )
257 24 24 256 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( 𝐾 ×t 𝐾 ) ∈ ( TopOn ‘ ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) ) )
258 iscn ⊢ ( ( ( 𝐾 ×t 𝐾 ) ∈ ( TopOn ‘ ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) ) ∧ 𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝐻 ) ) ) → ( ( -g ‘ 𝐻 ) ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) ↔ ( ( -g ‘ 𝐻 ) : ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) ⟶ ( Base ‘ 𝐻 ) ∧ ∀ 𝑢 ∈ 𝐾 ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ∈ ( 𝐾 ×t 𝐾 ) ) ) )
259 257 24 258 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( ( -g ‘ 𝐻 ) ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) ↔ ( ( -g ‘ 𝐻 ) : ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) ⟶ ( Base ‘ 𝐻 ) ∧ ∀ 𝑢 ∈ 𝐾 ( ◡ ( -g ‘ 𝐻 ) “ 𝑢 ) ∈ ( 𝐾 ×t 𝐾 ) ) ) )
260 30 255 259 mpbir2and ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( -g ‘ 𝐻 ) ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) )
261 4 28 istgp2 ⊢ ( 𝐻 ∈ TopGrp ↔ ( 𝐻 ∈ Grp ∧ 𝐻 ∈ TopSp ∧ ( -g ‘ 𝐻 ) ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) ) )
262 8 27 260 261 syl3anbrc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝐻 ∈ TopGrp )