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 syl5bir ( ∀ 𝑡 ∈ ( 𝑢 ) ∃ 𝑐𝐽𝑑𝐽 ( 𝑡 ∈ ( 𝑐 × 𝑑 ) ∧ ( 𝑐 × 𝑑 ) ⊆ ( 𝑢 ) ) → ( ( ( 𝑎𝑋𝑏𝑋 ) ∧ [ ( 𝑎 ( -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 )