Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  qustgplem Structured version   Visualization version   GIF version

Theorem qustgplem 22144
 Description: Lemma for qustgp 22145. (Contributed by Mario Carneiro, 18-Sep-2015.)
Hypotheses
Ref Expression
qustgp.h 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌))
qustgpopn.x 𝑋 = (Base‘𝐺)
qustgpopn.j 𝐽 = (TopOpen‘𝐺)
qustgpopn.k 𝐾 = (TopOpen‘𝐻)
qustgpopn.f 𝐹 = (𝑥𝑋 ↦ [𝑥](𝐺 ~QG 𝑌))
qustgplem.m = (𝑧𝑋, 𝑤𝑋 ↦ [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌))
Assertion
Ref Expression
qustgplem ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopGrp)
Distinct variable groups:   𝑥,𝑤,𝑧,𝐺   𝑤,𝐽,𝑥,𝑧   𝑤,𝐹,𝑧   𝑤,𝑋,𝑥,𝑧   𝑤,𝐻,𝑥,𝑧   𝑤,𝐾,𝑥,𝑧   𝑤,𝑌,𝑥,𝑧
Allowed substitution hints:   𝐹(𝑥)   (𝑥,𝑧,𝑤)

Proof of Theorem qustgplem
Dummy variables 𝑡 𝑏 𝑎 𝑐 𝑑 𝑝 𝑞 𝑟 𝑠 𝑢 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 qustgp.h . . . 4 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌))
21qusgrp 17857 . . 3 (𝑌 ∈ (NrmSGrp‘𝐺) → 𝐻 ∈ Grp)
32adantl 467 . 2 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ Grp)
41a1i 11 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌)))
5 qustgpopn.x . . . . . . . 8 𝑋 = (Base‘𝐺)
65a1i 11 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝑋 = (Base‘𝐺))
7 qustgpopn.f . . . . . . 7 𝐹 = (𝑥𝑋 ↦ [𝑥](𝐺 ~QG 𝑌))
8 ovex 6823 . . . . . . . 8 (𝐺 ~QG 𝑌) ∈ V
98a1i 11 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐺 ~QG 𝑌) ∈ V)
10 simpl 468 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐺 ∈ TopGrp)
114, 6, 7, 9, 10qusval 16410 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 = (𝐹s 𝐺))
124, 6, 7, 9, 10quslem 16411 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹:𝑋onto→(𝑋 / (𝐺 ~QG 𝑌)))
13 qustgpopn.j . . . . . 6 𝐽 = (TopOpen‘𝐺)
14 qustgpopn.k . . . . . 6 𝐾 = (TopOpen‘𝐻)
1511, 6, 12, 10, 13, 14imastopn 21744 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 = (𝐽 qTop 𝐹))
1613, 5tgptopon 22106 . . . . . . 7 (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋))
1716adantr 466 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐽 ∈ (TopOn‘𝑋))
18 qtoptopon 21728 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto→(𝑋 / (𝐺 ~QG 𝑌))) → (𝐽 qTop 𝐹) ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))))
1917, 12, 18syl2anc 573 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐽 qTop 𝐹) ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))))
2015, 19eqeltrd 2850 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))))
214, 6, 9, 10qusbas 16413 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑋 / (𝐺 ~QG 𝑌)) = (Base‘𝐻))
2221fveq2d 6336 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))) = (TopOn‘(Base‘𝐻)))
2320, 22eleqtrd 2852 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 ∈ (TopOn‘(Base‘𝐻)))
24 eqid 2771 . . . 4 (Base‘𝐻) = (Base‘𝐻)
2524, 14istps 20959 . . 3 (𝐻 ∈ TopSp ↔ 𝐾 ∈ (TopOn‘(Base‘𝐻)))
2623, 25sylibr 224 . 2 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopSp)
27 eqid 2771 . . . . 5 (-g𝐻) = (-g𝐻)
2824, 27grpsubf 17702 . . . 4 (𝐻 ∈ Grp → (-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻))
293, 28syl 17 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻))
30 cnvimass 5626 . . . . . . . . 9 ((-g𝐻) “ 𝑢) ⊆ dom (-g𝐻)
31 fdm 6191 . . . . . . . . . . 11 ((-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) → dom (-g𝐻) = ((Base‘𝐻) × (Base‘𝐻)))
3229, 31syl 17 . . . . . . . . . 10 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → dom (-g𝐻) = ((Base‘𝐻) × (Base‘𝐻)))
3332adantr 466 . . . . . . . . 9 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → dom (-g𝐻) = ((Base‘𝐻) × (Base‘𝐻)))
3430, 33syl5sseq 3802 . . . . . . . 8 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ((-g𝐻) “ 𝑢) ⊆ ((Base‘𝐻) × (Base‘𝐻)))
35 relxp 5266 . . . . . . . 8 Rel ((Base‘𝐻) × (Base‘𝐻))
36 relss 5346 . . . . . . . 8 (((-g𝐻) “ 𝑢) ⊆ ((Base‘𝐻) × (Base‘𝐻)) → (Rel ((Base‘𝐻) × (Base‘𝐻)) → Rel ((-g𝐻) “ 𝑢)))
3734, 35, 36mpisyl 21 . . . . . . 7 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → Rel ((-g𝐻) “ 𝑢))
3834sseld 3751 . . . . . . . 8 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐻) × (Base‘𝐻))))
39 vex 3354 . . . . . . . . . . . . . 14 𝑥 ∈ V
4039elqs 7951 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ ∃𝑎𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌))
4121adantr 466 . . . . . . . . . . . . . 14 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (𝑋 / (𝐺 ~QG 𝑌)) = (Base‘𝐻))
4241eleq2d 2836 . . . . . . . . . . . . 13 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (𝑥 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ 𝑥 ∈ (Base‘𝐻)))
4340, 42syl5bbr 274 . . . . . . . . . . . 12 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (∃𝑎𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ↔ 𝑥 ∈ (Base‘𝐻)))
44 vex 3354 . . . . . . . . . . . . . 14 𝑦 ∈ V
4544elqs 7951 . . . . . . . . . . . . 13 (𝑦 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ ∃𝑏𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌))
4641eleq2d 2836 . . . . . . . . . . . . 13 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (𝑦 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ 𝑦 ∈ (Base‘𝐻)))
4745, 46syl5bbr 274 . . . . . . . . . . . 12 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (∃𝑏𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌) ↔ 𝑦 ∈ (Base‘𝐻)))
4843, 47anbi12d 616 . . . . . . . . . . 11 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ((∃𝑎𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ ∃𝑏𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))))
49 reeanv 3255 . . . . . . . . . . 11 (∃𝑎𝑋𝑏𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ (∃𝑎𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ ∃𝑏𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌)))
50 opelxp 5286 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻)))
5148, 49, 503bitr4g 303 . . . . . . . . . 10 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (∃𝑎𝑋𝑏𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐻) × (Base‘𝐻))))
523ad2antrr 705 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝐻 ∈ Grp)
5352, 28syl 17 . . . . . . . . . . . . . 14 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻))
54 ffn 6185 . . . . . . . . . . . . . 14 ((-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) → (-g𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)))
55 elpreima 6480 . . . . . . . . . . . . . 14 ((-g𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)) → (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧ ((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩) ∈ 𝑢)))
5653, 54, 553syl 18 . . . . . . . . . . . . 13 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧ ((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩) ∈ 𝑢)))
57 df-ov 6796 . . . . . . . . . . . . . . . . 17 ([𝑎](𝐺 ~QG 𝑌)(-g𝐻)[𝑏](𝐺 ~QG 𝑌)) = ((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩)
58 simpllr 760 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝑌 ∈ (NrmSGrp‘𝐺))
59 simprl 754 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝑎𝑋)
60 simprr 756 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝑏𝑋)
61 eqid 2771 . . . . . . . . . . . . . . . . . . 19 (-g𝐺) = (-g𝐺)
621, 5, 61, 27qussub 17862 . . . . . . . . . . . . . . . . . 18 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑎𝑋𝑏𝑋) → ([𝑎](𝐺 ~QG 𝑌)(-g𝐻)[𝑏](𝐺 ~QG 𝑌)) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
6358, 59, 60, 62syl3anc 1476 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ([𝑎](𝐺 ~QG 𝑌)(-g𝐻)[𝑏](𝐺 ~QG 𝑌)) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
6457, 63syl5eqr 2819 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
6564eleq1d 2835 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩) ∈ 𝑢 ↔ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢))
66 simpr 471 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (𝑎𝑋𝑏𝑋))
67 qustgplem.m . . . . . . . . . . . . . . . . . . . . . 22 = (𝑧𝑋, 𝑤𝑋 ↦ [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌))
68 tgpgrp 22102 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
6968adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐺 ∈ Grp)
705, 61grpsubf 17702 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐺 ∈ Grp → (-g𝐺):(𝑋 × 𝑋)⟶𝑋)
71 ffn 6185 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((-g𝐺):(𝑋 × 𝑋)⟶𝑋 → (-g𝐺) Fn (𝑋 × 𝑋))
7269, 70, 713syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐺) Fn (𝑋 × 𝑋))
73 fnov 6915 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((-g𝐺) Fn (𝑋 × 𝑋) ↔ (-g𝐺) = (𝑧𝑋, 𝑤𝑋 ↦ (𝑧(-g𝐺)𝑤)))
7472, 73sylib 208 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐺) = (𝑧𝑋, 𝑤𝑋 ↦ (𝑧(-g𝐺)𝑤)))
7513, 61tgpsubcn 22114 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐺 ∈ TopGrp → (-g𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
7675adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
7774, 76eqeltrrd 2851 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑧𝑋, 𝑤𝑋 ↦ (𝑧(-g𝐺)𝑤)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
78 ecexg 7900 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐺 ~QG 𝑌) ∈ V → [𝑥](𝐺 ~QG 𝑌) ∈ V)
798, 78ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 [𝑥](𝐺 ~QG 𝑌) ∈ V
8079, 7fnmpti 6162 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝐹 Fn 𝑋
81 qtopid 21729 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 Fn 𝑋) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)))
8217, 80, 81sylancl 574 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)))
8315oveq2d 6809 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐽 Cn 𝐾) = (𝐽 Cn (𝐽 qTop 𝐹)))
8482, 83eleqtrrd 2853 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹 ∈ (𝐽 Cn 𝐾))
857, 84syl5eqelr 2855 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑥𝑋 ↦ [𝑥](𝐺 ~QG 𝑌)) ∈ (𝐽 Cn 𝐾))
86 eceq1 7934 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑧(-g𝐺)𝑤) → [𝑥](𝐺 ~QG 𝑌) = [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌))
8717, 17, 77, 17, 85, 86cnmpt21 21695 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑧𝑋, 𝑤𝑋 ↦ [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌)) ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
8867, 87syl5eqel 2854 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
8988ad2antrr 705 . . . . . . . . . . . . . . . . . . . 20 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
90 simplr 752 . . . . . . . . . . . . . . . . . . . 20 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝑢𝐾)
91 cnima 21290 . . . . . . . . . . . . . . . . . . . 20 (( ∈ ((𝐽 ×t 𝐽) Cn 𝐾) ∧ 𝑢𝐾) → ( 𝑢) ∈ (𝐽 ×t 𝐽))
9289, 90, 91syl2anc 573 . . . . . . . . . . . . . . . . . . 19 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ( 𝑢) ∈ (𝐽 ×t 𝐽))
9317ad2antrr 705 . . . . . . . . . . . . . . . . . . . 20 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
94 eltx 21592 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘𝑋)) → (( 𝑢) ∈ (𝐽 ×t 𝐽) ↔ ∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
9593, 93, 94syl2anc 573 . . . . . . . . . . . . . . . . . . 19 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (( 𝑢) ∈ (𝐽 ×t 𝐽) ↔ ∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
9692, 95mpbid 222 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))
97 ecexg 7900 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ~QG 𝑌) ∈ V → [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌) ∈ V)
988, 97ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌) ∈ V
9967, 98fnmpt2i 7389 . . . . . . . . . . . . . . . . . . . . 21 Fn (𝑋 × 𝑋)
100 elpreima 6480 . . . . . . . . . . . . . . . . . . . . 21 ( Fn (𝑋 × 𝑋) → (⟨𝑎, 𝑏⟩ ∈ ( 𝑢) ↔ (⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢)))
10199, 100ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑎, 𝑏⟩ ∈ ( 𝑢) ↔ (⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢))
102 opelxp 5286 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋) ↔ (𝑎𝑋𝑏𝑋))
103102anbi1i 610 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢) ↔ ((𝑎𝑋𝑏𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢))
104 df-ov 6796 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 𝑏) = ( ‘⟨𝑎, 𝑏⟩)
105 oveq12 6802 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑧 = 𝑎𝑤 = 𝑏) → (𝑧(-g𝐺)𝑤) = (𝑎(-g𝐺)𝑏))
106105eceq1d 7935 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 = 𝑎𝑤 = 𝑏) → [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
107 ecexg 7900 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ~QG 𝑌) ∈ V → [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ V)
1088, 107ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ V
109106, 67, 108ovmpt2a 6938 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝑋𝑏𝑋) → (𝑎 𝑏) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
110104, 109syl5eqr 2819 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎𝑋𝑏𝑋) → ( ‘⟨𝑎, 𝑏⟩) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
111110eleq1d 2835 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎𝑋𝑏𝑋) → (( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢 ↔ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢))
112111pm5.32i 564 . . . . . . . . . . . . . . . . . . . 20 (((𝑎𝑋𝑏𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢) ↔ ((𝑎𝑋𝑏𝑋) ∧ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢))
113101, 103, 1123bitri 286 . . . . . . . . . . . . . . . . . . 19 (⟨𝑎, 𝑏⟩ ∈ ( 𝑢) ↔ ((𝑎𝑋𝑏𝑋) ∧ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢))
114 eleq1 2838 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑡 ∈ (𝑐 × 𝑑) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑)))
115 opelxp 5286 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ↔ (𝑎𝑐𝑏𝑑))
116114, 115syl6bb 276 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑡 ∈ (𝑐 × 𝑑) ↔ (𝑎𝑐𝑏𝑑)))
117116anbi1d 615 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) ↔ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
1181172rexbidv 3205 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = ⟨𝑎, 𝑏⟩ → (∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) ↔ ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
119118rspccv 3457 . . . . . . . . . . . . . . . . . . 19 (∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) → (⟨𝑎, 𝑏⟩ ∈ ( 𝑢) → ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
120113, 119syl5bir 233 . . . . . . . . . . . . . . . . . 18 (∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) → (((𝑎𝑋𝑏𝑋) ∧ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢) → ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
12196, 120syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (((𝑎𝑋𝑏𝑋) ∧ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢) → ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
12266, 121mpand 675 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ([(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢 → ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
123 simp-4l 768 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝐺 ∈ TopGrp)
12458adantr 466 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑌 ∈ (NrmSGrp‘𝐺))
125 simprll 764 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑐𝐽)
1261, 5, 13, 14, 7qustgpopn 22143 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑐𝐽) → (𝐹𝑐) ∈ 𝐾)
127123, 124, 125, 126syl3anc 1476 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑐) ∈ 𝐾)
128 simprlr 765 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑑𝐽)
1291, 5, 13, 14, 7qustgpopn 22143 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑑𝐽) → (𝐹𝑑) ∈ 𝐾)
130123, 124, 128, 129syl3anc 1476 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑑) ∈ 𝐾)
13159adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑎𝑋)
132 eceq1 7934 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑎 → [𝑥](𝐺 ~QG 𝑌) = [𝑎](𝐺 ~QG 𝑌))
133132, 7, 79fvmpt3i 6429 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎𝑋 → (𝐹𝑎) = [𝑎](𝐺 ~QG 𝑌))
134131, 133syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑎) = [𝑎](𝐺 ~QG 𝑌))
135123, 16syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝐽 ∈ (TopOn‘𝑋))
136 toponss 20952 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑐𝐽) → 𝑐𝑋)
137135, 125, 136syl2anc 573 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑐𝑋)
138 simprrl 766 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝑎𝑐𝑏𝑑))
139138simpld 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑎𝑐)
140 fnfvima 6639 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 Fn 𝑋𝑐𝑋𝑎𝑐) → (𝐹𝑎) ∈ (𝐹𝑐))
14180, 140mp3an1 1559 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑐𝑋𝑎𝑐) → (𝐹𝑎) ∈ (𝐹𝑐))
142137, 139, 141syl2anc 573 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑎) ∈ (𝐹𝑐))
143134, 142eqeltrrd 2851 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → [𝑎](𝐺 ~QG 𝑌) ∈ (𝐹𝑐))
14460adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑏𝑋)
145 eceq1 7934 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑏 → [𝑥](𝐺 ~QG 𝑌) = [𝑏](𝐺 ~QG 𝑌))
146145, 7, 79fvmpt3i 6429 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏𝑋 → (𝐹𝑏) = [𝑏](𝐺 ~QG 𝑌))
147144, 146syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑏) = [𝑏](𝐺 ~QG 𝑌))
148 toponss 20952 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑑𝐽) → 𝑑𝑋)
149135, 128, 148syl2anc 573 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑑𝑋)
150138simprd 483 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑏𝑑)
151 fnfvima 6639 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 Fn 𝑋𝑑𝑋𝑏𝑑) → (𝐹𝑏) ∈ (𝐹𝑑))
15280, 151mp3an1 1559 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑑𝑋𝑏𝑑) → (𝐹𝑏) ∈ (𝐹𝑑))
153149, 150, 152syl2anc 573 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑏) ∈ (𝐹𝑑))
154147, 153eqeltrrd 2851 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → [𝑏](𝐺 ~QG 𝑌) ∈ (𝐹𝑑))
155 opelxpi 5288 . . . . . . . . . . . . . . . . . . . 20 (([𝑎](𝐺 ~QG 𝑌) ∈ (𝐹𝑐) ∧ [𝑏](𝐺 ~QG 𝑌) ∈ (𝐹𝑑)) → ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑)))
156143, 154, 155syl2anc 573 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑)))
157137sselda 3752 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ 𝑝𝑐) → 𝑝𝑋)
158149sselda 3752 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ 𝑞𝑑) → 𝑞𝑋)
159157, 158anim12dan 605 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → (𝑝𝑋𝑞𝑋))
160 eceq1 7934 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑝 → [𝑥](𝐺 ~QG 𝑌) = [𝑝](𝐺 ~QG 𝑌))
161160, 7, 79fvmpt3i 6429 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝𝑋 → (𝐹𝑝) = [𝑝](𝐺 ~QG 𝑌))
162 eceq1 7934 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑞 → [𝑥](𝐺 ~QG 𝑌) = [𝑞](𝐺 ~QG 𝑌))
163162, 7, 79fvmpt3i 6429 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑞𝑋 → (𝐹𝑞) = [𝑞](𝐺 ~QG 𝑌))
164 opeq12 4541 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹𝑝) = [𝑝](𝐺 ~QG 𝑌) ∧ (𝐹𝑞) = [𝑞](𝐺 ~QG 𝑌)) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ = ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩)
165161, 163, 164syl2an 583 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑝𝑋𝑞𝑋) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ = ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩)
166159, 165syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ = ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩)
167124adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → 𝑌 ∈ (NrmSGrp‘𝐺))
1681, 5, 24quseccl 17858 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑝𝑋) → [𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻))
1691, 5, 24quseccl 17858 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑞𝑋) → [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻))
170168, 169anim12dan 605 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝑝𝑋𝑞𝑋)) → ([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)))
171167, 159, 170syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)))
172 opelxpi 5288 . . . . . . . . . . . . . . . . . . . . . . . . 25 (([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)) → ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)))
173171, 172syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)))
1741, 5, 61, 27qussub 17862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑝𝑋𝑞𝑋) → ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
1751743expb 1113 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝑝𝑋𝑞𝑋)) → ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
176167, 159, 175syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
177 oveq12 6802 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 = 𝑝𝑤 = 𝑞) → (𝑧(-g𝐺)𝑤) = (𝑝(-g𝐺)𝑞))
178177eceq1d 7935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑧 = 𝑝𝑤 = 𝑞) → [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
179 ecexg 7900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐺 ~QG 𝑌) ∈ V → [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌) ∈ V)
1808, 179ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌) ∈ V
181178, 67, 180ovmpt2a 6938 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑝𝑋𝑞𝑋) → (𝑝 𝑞) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
182159, 181syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → (𝑝 𝑞) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
183176, 182eqtr4d 2808 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = (𝑝 𝑞))
184 df-ov 6796 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = ((-g𝐻)‘⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩)
185 df-ov 6796 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 𝑞) = ( ‘⟨𝑝, 𝑞⟩)
186183, 184, 1853eqtr3g 2828 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ((-g𝐻)‘⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩) = ( ‘⟨𝑝, 𝑞⟩))
187 opelxpi 5288 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑝𝑐𝑞𝑑) → ⟨𝑝, 𝑞⟩ ∈ (𝑐 × 𝑑))
188 simprrr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝑐 × 𝑑) ⊆ ( 𝑢))
189188sselda 3752 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ ⟨𝑝, 𝑞⟩ ∈ (𝑐 × 𝑑)) → ⟨𝑝, 𝑞⟩ ∈ ( 𝑢))
190187, 189sylan2 580 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨𝑝, 𝑞⟩ ∈ ( 𝑢))
191 elpreima 6480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( Fn (𝑋 × 𝑋) → (⟨𝑝, 𝑞⟩ ∈ ( 𝑢) ↔ (⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑝, 𝑞⟩) ∈ 𝑢)))
19299, 191ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟨𝑝, 𝑞⟩ ∈ ( 𝑢) ↔ (⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑝, 𝑞⟩) ∈ 𝑢))
193192simprbi 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑝, 𝑞⟩ ∈ ( 𝑢) → ( ‘⟨𝑝, 𝑞⟩) ∈ 𝑢)
194190, 193syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ( ‘⟨𝑝, 𝑞⟩) ∈ 𝑢)
195186, 194eqeltrd 2850 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ((-g𝐻)‘⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩) ∈ 𝑢)
19653, 54syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (-g𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)))
197196ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → (-g𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)))
198 elpreima 6480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((-g𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)) → (⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢) ↔ (⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧ ((-g𝐻)‘⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩) ∈ 𝑢)))
199197, 198syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → (⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢) ↔ (⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧ ((-g𝐻)‘⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩) ∈ 𝑢)))
200173, 195, 199mpbir2and 692 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢))
201166, 200eqeltrd 2850 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢))
202201ralrimivva 3120 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ∀𝑝𝑐𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢))
203 opeq1 4539 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = (𝐹𝑝) → ⟨𝑧, 𝑤⟩ = ⟨(𝐹𝑝), 𝑤⟩)
204203eleq1d 2835 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = (𝐹𝑝) → (⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
205204ralbidv 3135 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (𝐹𝑝) → (∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
206205ralima 6641 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 Fn 𝑋𝑐𝑋) → (∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
20780, 206mpan 670 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐𝑋 → (∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
208 opeq2 4540 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = (𝐹𝑞) → ⟨(𝐹𝑝), 𝑤⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩)
209208eleq1d 2835 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = (𝐹𝑞) → (⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
210209ralima 6641 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 Fn 𝑋𝑑𝑋) → (∀𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
21180, 210mpan 670 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑𝑋 → (∀𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
212211ralbidv 3135 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑𝑋 → (∀𝑝𝑐𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
213207, 212sylan9bb 499 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑐𝑋𝑑𝑋) → (∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
214137, 149, 213syl2anc 573 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
215202, 214mpbird 247 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢))
216 dfss3 3741 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢) ↔ ∀𝑦 ∈ ((𝐹𝑐) × (𝐹𝑑))𝑦 ∈ ((-g𝐻) “ 𝑢))
217 eleq1 2838 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = ⟨𝑧, 𝑤⟩ → (𝑦 ∈ ((-g𝐻) “ 𝑢) ↔ ⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
218217ralxp 5402 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦 ∈ ((𝐹𝑐) × (𝐹𝑑))𝑦 ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢))
219216, 218bitri 264 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢) ↔ ∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢))
220215, 219sylibr 224 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢))
221 xpeq1 5263 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟 = (𝐹𝑐) → (𝑟 × 𝑠) = ((𝐹𝑐) × 𝑠))
222221eleq2d 2836 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = (𝐹𝑐) → (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × 𝑠)))
223221sseq1d 3781 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = (𝐹𝑐) → ((𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢) ↔ ((𝐹𝑐) × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
224222, 223anbi12d 616 . . . . . . . . . . . . . . . . . . . 20 (𝑟 = (𝐹𝑐) → ((⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × 𝑠) ∧ ((𝐹𝑐) × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
225 xpeq2 5269 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝐹𝑑) → ((𝐹𝑐) × 𝑠) = ((𝐹𝑐) × (𝐹𝑑)))
226225eleq2d 2836 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝐹𝑑) → (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × 𝑠) ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑))))
227225sseq1d 3781 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝐹𝑑) → (((𝐹𝑐) × 𝑠) ⊆ ((-g𝐻) “ 𝑢) ↔ ((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢)))
228226, 227anbi12d 616 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = (𝐹𝑑) → ((⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × 𝑠) ∧ ((𝐹𝑐) × 𝑠) ⊆ ((-g𝐻) “ 𝑢)) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑)) ∧ ((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢))))
229224, 228rspc2ev 3474 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑐) ∈ 𝐾 ∧ (𝐹𝑑) ∈ 𝐾 ∧ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑)) ∧ ((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢))) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
230127, 130, 156, 220, 229syl112anc 1480 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
231230expr 444 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑐𝐽𝑑𝐽)) → (((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
232231rexlimdvva 3186 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
233122, 232syld 47 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ([(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢 → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
23465, 233sylbid 230 . . . . . . . . . . . . . 14 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩) ∈ 𝑢 → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
235234adantld 478 . . . . . . . . . . . . 13 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ((⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧ ((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩) ∈ 𝑢) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
23656, 235sylbid 230 . . . . . . . . . . . 12 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
237 opeq12 4541 . . . . . . . . . . . . . 14 ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → ⟨𝑥, 𝑦⟩ = ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩)
238237eleq1d 2835 . . . . . . . . . . . . 13 ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢)))
239237eleq1d 2835 . . . . . . . . . . . . . 14 ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))} ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))}))
240 opex 5060 . . . . . . . . . . . . . . 15 ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ V
241 eleq1 2838 . . . . . . . . . . . . . . . . 17 (𝑤 = ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ → (𝑤 ∈ (𝑟 × 𝑠) ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠)))
242241anbi1d 615 . . . . . . . . . . . . . . . 16 (𝑤 = ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ → ((𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
2432422rexbidv 3205 . . . . . . . . . . . . . . 15 (𝑤 = ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ → (∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)) ↔ ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
244240, 243elab 3501 . . . . . . . . . . . . . 14 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))} ↔ ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
245239, 244syl6bb 276 . . . . . . . . . . . . 13 ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))} ↔ ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
246238, 245imbi12d 333 . . . . . . . . . . . 12 ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → ((⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) → ⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))}) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))))
247236, 246syl5ibrcom 237 . . . . . . . . . . 11 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) → ⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))})))
248247rexlimdvva 3186 . . . . . . . . . 10 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (∃𝑎𝑋𝑏𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) → ⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))})))
24951, 248sylbird 250 . . . . . . . . 9 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) → ⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))})))
250249com23 86 . . . . . . . 8 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) → (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)) → ⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))})))
25138, 250mpdd 43 . . . . . . 7 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) → ⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))}))
25237, 251relssdv 5352 . . . . . 6 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ((-g𝐻) “ 𝑢) ⊆ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))})
253 ssabral 3822 . . . . . 6 (((-g𝐻) “ 𝑢) ⊆ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))} ↔ ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
254252, 253sylib 208 . . . . 5 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
255 eltx 21592 . . . . . . 7 ((𝐾 ∈ (TopOn‘(Base‘𝐻)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → (((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
25623, 23, 255syl2anc 573 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
257256adantr 466 . . . . 5 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
258254, 257mpbird 247 . . . 4 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾))
259258ralrimiva 3115 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ∀𝑢𝐾 ((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾))
260 txtopon 21615 . . . . 5 ((𝐾 ∈ (TopOn‘(Base‘𝐻)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → (𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻))))
26123, 23, 260syl2anc 573 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻))))
262 iscn 21260 . . . 4 (((𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻))) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → ((-g𝐻) ∈ ((𝐾 ×t 𝐾) Cn 𝐾) ↔ ((-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) ∧ ∀𝑢𝐾 ((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾))))
263261, 23, 262syl2anc 573 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ((-g𝐻) ∈ ((𝐾 ×t 𝐾) Cn 𝐾) ↔ ((-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) ∧ ∀𝑢𝐾 ((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾))))
26429, 259, 263mpbir2and 692 . 2 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐻) ∈ ((𝐾 ×t 𝐾) Cn 𝐾))
26514, 27istgp2 22115 . 2 (𝐻 ∈ TopGrp ↔ (𝐻 ∈ Grp ∧ 𝐻 ∈ TopSp ∧ (-g𝐻) ∈ ((𝐾 ×t 𝐾) Cn 𝐾)))
2663, 26, 264, 265syl3anbrc 1428 1 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopGrp)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   = wceq 1631   ∈ wcel 2145  {cab 2757  ∀wral 3061  ∃wrex 3062  Vcvv 3351   ⊆ wss 3723  ⟨cop 4322   ↦ cmpt 4863   × cxp 5247  ◡ccnv 5248  dom cdm 5249   “ cima 5252  Rel wrel 5254   Fn wfn 6026  ⟶wf 6027  –onto→wfo 6029  ‘cfv 6031  (class class class)co 6793   ↦ cmpt2 6795  [cec 7894   / cqs 7895  Basecbs 16064  TopOpenctopn 16290   qTop cqtop 16371   /s cqus 16373  Grpcgrp 17630  -gcsg 17632  NrmSGrpcnsg 17797   ~QG cqg 17798  TopOnctopon 20935  TopSpctps 20957   Cn ccn 21249   ×t ctx 21584  TopGrpctgp 22095 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-tpos 7504  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-oadd 7717  df-er 7896  df-ec 7898  df-qs 7902  df-map 8011  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-sup 8504  df-inf 8505  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-nn 11223  df-2 11281  df-3 11282  df-4 11283  df-5 11284  df-6 11285  df-7 11286  df-8 11287  df-9 11288  df-n0 11495  df-z 11580  df-dec 11696  df-uz 11889  df-fz 12534  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-mulr 16163  df-sca 16165  df-vsca 16166  df-ip 16167  df-tset 16168  df-ple 16169  df-ds 16172  df-rest 16291  df-topn 16292  df-0g 16310  df-topgen 16312  df-qtop 16375  df-imas 16376  df-qus 16377  df-plusf 17449  df-mgm 17450  df-sgrp 17492  df-mnd 17503  df-grp 17633  df-minusg 17634  df-sbg 17635  df-subg 17799  df-nsg 17800  df-eqg 17801  df-oppg 17983  df-top 20919  df-topon 20936  df-topsp 20958  df-bases 20971  df-cn 21252  df-cnp 21253  df-tx 21586  df-hmeo 21779  df-tmd 22096  df-tgp 22097 This theorem is referenced by:  qustgp  22145
 Copyright terms: Public domain W3C validator