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

Theorem qustgplem 21847
Description: Lemma for qustgp 21848. (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 17581 . . 3 (𝑌 ∈ (NrmSGrp‘𝐺) → 𝐻 ∈ Grp)
32adantl 482 . 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 6638 . . . . . . . 8 (𝐺 ~QG 𝑌) ∈ V
98a1i 11 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐺 ~QG 𝑌) ∈ V)
10 simpl 473 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐺 ∈ TopGrp)
114, 6, 7, 9, 10qusval 16134 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 = (𝐹s 𝐺))
124, 6, 7, 9, 10quslem 16135 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹:𝑋onto→(𝑋 / (𝐺 ~QG 𝑌)))
13 qustgpopn.j . . . . . 6 𝐽 = (TopOpen‘𝐺)
14 qustgpopn.k . . . . . 6 𝐾 = (TopOpen‘𝐻)
1511, 6, 12, 10, 13, 14imastopn 21446 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 = (𝐽 qTop 𝐹))
1613, 5tgptopon 21809 . . . . . . 7 (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋))
1716adantr 481 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐽 ∈ (TopOn‘𝑋))
18 qtoptopon 21430 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto→(𝑋 / (𝐺 ~QG 𝑌))) → (𝐽 qTop 𝐹) ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))))
1917, 12, 18syl2anc 692 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐽 qTop 𝐹) ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))))
2015, 19eqeltrd 2698 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))))
214, 6, 9, 10qusbas 16137 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑋 / (𝐺 ~QG 𝑌)) = (Base‘𝐻))
2221fveq2d 6157 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))) = (TopOn‘(Base‘𝐻)))
2320, 22eleqtrd 2700 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 ∈ (TopOn‘(Base‘𝐻)))
24 eqid 2621 . . . 4 (Base‘𝐻) = (Base‘𝐻)
2524, 14istps 20662 . . 3 (𝐻 ∈ TopSp ↔ 𝐾 ∈ (TopOn‘(Base‘𝐻)))
2623, 25sylibr 224 . 2 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopSp)
27 eqid 2621 . . . . 5 (-g𝐻) = (-g𝐻)
2824, 27grpsubf 17426 . . . 4 (𝐻 ∈ Grp → (-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻))
293, 28syl 17 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻))
30 cnvimass 5449 . . . . . . . . 9 ((-g𝐻) “ 𝑢) ⊆ dom (-g𝐻)
31 fdm 6013 . . . . . . . . . . 11 ((-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) → dom (-g𝐻) = ((Base‘𝐻) × (Base‘𝐻)))
3229, 31syl 17 . . . . . . . . . 10 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → dom (-g𝐻) = ((Base‘𝐻) × (Base‘𝐻)))
3332adantr 481 . . . . . . . . 9 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → dom (-g𝐻) = ((Base‘𝐻) × (Base‘𝐻)))
3430, 33syl5sseq 3637 . . . . . . . 8 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ((-g𝐻) “ 𝑢) ⊆ ((Base‘𝐻) × (Base‘𝐻)))
35 relxp 5193 . . . . . . . 8 Rel ((Base‘𝐻) × (Base‘𝐻))
36 relss 5172 . . . . . . . 8 (((-g𝐻) “ 𝑢) ⊆ ((Base‘𝐻) × (Base‘𝐻)) → (Rel ((Base‘𝐻) × (Base‘𝐻)) → Rel ((-g𝐻) “ 𝑢)))
3734, 35, 36mpisyl 21 . . . . . . 7 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → Rel ((-g𝐻) “ 𝑢))
3834sseld 3586 . . . . . . . 8 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐻) × (Base‘𝐻))))
39 vex 3192 . . . . . . . . . . . . . 14 𝑥 ∈ V
4039elqs 7751 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ ∃𝑎𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌))
4121adantr 481 . . . . . . . . . . . . . 14 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (𝑋 / (𝐺 ~QG 𝑌)) = (Base‘𝐻))
4241eleq2d 2684 . . . . . . . . . . . . 13 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (𝑥 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ 𝑥 ∈ (Base‘𝐻)))
4340, 42syl5bbr 274 . . . . . . . . . . . 12 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (∃𝑎𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ↔ 𝑥 ∈ (Base‘𝐻)))
44 vex 3192 . . . . . . . . . . . . . 14 𝑦 ∈ V
4544elqs 7751 . . . . . . . . . . . . 13 (𝑦 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ ∃𝑏𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌))
4641eleq2d 2684 . . . . . . . . . . . . 13 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (𝑦 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ 𝑦 ∈ (Base‘𝐻)))
4745, 46syl5bbr 274 . . . . . . . . . . . 12 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (∃𝑏𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌) ↔ 𝑦 ∈ (Base‘𝐻)))
4843, 47anbi12d 746 . . . . . . . . . . 11 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ((∃𝑎𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ ∃𝑏𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))))
49 reeanv 3100 . . . . . . . . . . 11 (∃𝑎𝑋𝑏𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ (∃𝑎𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ ∃𝑏𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌)))
50 opelxp 5111 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻)))
5148, 49, 503bitr4g 303 . . . . . . . . . 10 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (∃𝑎𝑋𝑏𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐻) × (Base‘𝐻))))
523ad2antrr 761 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝐻 ∈ Grp)
5352, 28syl 17 . . . . . . . . . . . . . 14 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻))
54 ffn 6007 . . . . . . . . . . . . . 14 ((-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) → (-g𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)))
55 elpreima 6298 . . . . . . . . . . . . . 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 6613 . . . . . . . . . . . . . . . . 17 ([𝑎](𝐺 ~QG 𝑌)(-g𝐻)[𝑏](𝐺 ~QG 𝑌)) = ((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩)
58 simpllr 798 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝑌 ∈ (NrmSGrp‘𝐺))
59 simprl 793 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝑎𝑋)
60 simprr 795 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝑏𝑋)
61 eqid 2621 . . . . . . . . . . . . . . . . . . 19 (-g𝐺) = (-g𝐺)
621, 5, 61, 27qussub 17586 . . . . . . . . . . . . . . . . . 18 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑎𝑋𝑏𝑋) → ([𝑎](𝐺 ~QG 𝑌)(-g𝐻)[𝑏](𝐺 ~QG 𝑌)) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
6358, 59, 60, 62syl3anc 1323 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ([𝑎](𝐺 ~QG 𝑌)(-g𝐻)[𝑏](𝐺 ~QG 𝑌)) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
6457, 63syl5eqr 2669 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
6564eleq1d 2683 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩) ∈ 𝑢 ↔ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢))
66 simpr 477 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (𝑎𝑋𝑏𝑋))
67 qustgplem.m . . . . . . . . . . . . . . . . . . . . . 22 = (𝑧𝑋, 𝑤𝑋 ↦ [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌))
68 tgpgrp 21805 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
6968adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐺 ∈ Grp)
705, 61grpsubf 17426 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐺 ∈ Grp → (-g𝐺):(𝑋 × 𝑋)⟶𝑋)
71 ffn 6007 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((-g𝐺):(𝑋 × 𝑋)⟶𝑋 → (-g𝐺) Fn (𝑋 × 𝑋))
7269, 70, 713syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐺) Fn (𝑋 × 𝑋))
73 fnov 6728 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((-g𝐺) Fn (𝑋 × 𝑋) ↔ (-g𝐺) = (𝑧𝑋, 𝑤𝑋 ↦ (𝑧(-g𝐺)𝑤)))
7472, 73sylib 208 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐺) = (𝑧𝑋, 𝑤𝑋 ↦ (𝑧(-g𝐺)𝑤)))
7513, 61tgpsubcn 21817 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐺 ∈ TopGrp → (-g𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
7675adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
7774, 76eqeltrrd 2699 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑧𝑋, 𝑤𝑋 ↦ (𝑧(-g𝐺)𝑤)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
78 ecexg 7698 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐺 ~QG 𝑌) ∈ V → [𝑥](𝐺 ~QG 𝑌) ∈ V)
798, 78ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 [𝑥](𝐺 ~QG 𝑌) ∈ V
8079, 7fnmpti 5984 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝐹 Fn 𝑋
81 qtopid 21431 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 Fn 𝑋) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)))
8217, 80, 81sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)))
8315oveq2d 6626 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐽 Cn 𝐾) = (𝐽 Cn (𝐽 qTop 𝐹)))
8482, 83eleqtrrd 2701 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹 ∈ (𝐽 Cn 𝐾))
857, 84syl5eqelr 2703 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑥𝑋 ↦ [𝑥](𝐺 ~QG 𝑌)) ∈ (𝐽 Cn 𝐾))
86 eceq1 7734 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑧(-g𝐺)𝑤) → [𝑥](𝐺 ~QG 𝑌) = [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌))
8717, 17, 77, 17, 85, 86cnmpt21 21397 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑧𝑋, 𝑤𝑋 ↦ [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌)) ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
8867, 87syl5eqel 2702 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
8988ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
90 simplr 791 . . . . . . . . . . . . . . . . . . . 20 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝑢𝐾)
91 cnima 20992 . . . . . . . . . . . . . . . . . . . 20 (( ∈ ((𝐽 ×t 𝐽) Cn 𝐾) ∧ 𝑢𝐾) → ( 𝑢) ∈ (𝐽 ×t 𝐽))
9289, 90, 91syl2anc 692 . . . . . . . . . . . . . . . . . . 19 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ( 𝑢) ∈ (𝐽 ×t 𝐽))
9317ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
94 eltx 21294 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘𝑋)) → (( 𝑢) ∈ (𝐽 ×t 𝐽) ↔ ∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
9593, 93, 94syl2anc 692 . . . . . . . . . . . . . . . . . . 19 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (( 𝑢) ∈ (𝐽 ×t 𝐽) ↔ ∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
9692, 95mpbid 222 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))
97 ecexg 7698 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ~QG 𝑌) ∈ V → [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌) ∈ V)
988, 97ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌) ∈ V
9967, 98fnmpt2i 7191 . . . . . . . . . . . . . . . . . . . . 21 Fn (𝑋 × 𝑋)
100 elpreima 6298 . . . . . . . . . . . . . . . . . . . . 21 ( Fn (𝑋 × 𝑋) → (⟨𝑎, 𝑏⟩ ∈ ( 𝑢) ↔ (⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢)))
10199, 100ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑎, 𝑏⟩ ∈ ( 𝑢) ↔ (⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢))
102 opelxp 5111 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋) ↔ (𝑎𝑋𝑏𝑋))
103102anbi1i 730 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢) ↔ ((𝑎𝑋𝑏𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢))
104 df-ov 6613 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 𝑏) = ( ‘⟨𝑎, 𝑏⟩)
105 oveq12 6619 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑧 = 𝑎𝑤 = 𝑏) → (𝑧(-g𝐺)𝑤) = (𝑎(-g𝐺)𝑏))
106105eceq1d 7735 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 = 𝑎𝑤 = 𝑏) → [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
107 ecexg 7698 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ~QG 𝑌) ∈ V → [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ V)
1088, 107ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ V
109106, 67, 108ovmpt2a 6751 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝑋𝑏𝑋) → (𝑎 𝑏) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
110104, 109syl5eqr 2669 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎𝑋𝑏𝑋) → ( ‘⟨𝑎, 𝑏⟩) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
111110eleq1d 2683 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎𝑋𝑏𝑋) → (( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢 ↔ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢))
112111pm5.32i 668 . . . . . . . . . . . . . . . . . . . 20 (((𝑎𝑋𝑏𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢) ↔ ((𝑎𝑋𝑏𝑋) ∧ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢))
113101, 103, 1123bitri 286 . . . . . . . . . . . . . . . . . . 19 (⟨𝑎, 𝑏⟩ ∈ ( 𝑢) ↔ ((𝑎𝑋𝑏𝑋) ∧ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢))
114 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑡 ∈ (𝑐 × 𝑑) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑)))
115 opelxp 5111 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ↔ (𝑎𝑐𝑏𝑑))
116114, 115syl6bb 276 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑡 ∈ (𝑐 × 𝑑) ↔ (𝑎𝑐𝑏𝑑)))
117116anbi1d 740 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) ↔ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
1181172rexbidv 3051 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = ⟨𝑎, 𝑏⟩ → (∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) ↔ ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
119118rspccv 3295 . . . . . . . . . . . . . . . . . . 19 (∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) → (⟨𝑎, 𝑏⟩ ∈ ( 𝑢) → ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
120113, 119syl5bir 233 . . . . . . . . . . . . . . . . . 18 (∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) → (((𝑎𝑋𝑏𝑋) ∧ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢) → ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
12196, 120syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (((𝑎𝑋𝑏𝑋) ∧ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢) → ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
12266, 121mpand 710 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ([(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢 → ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
123 simp-4l 805 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝐺 ∈ TopGrp)
12458adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑌 ∈ (NrmSGrp‘𝐺))
125 simprll 801 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑐𝐽)
1261, 5, 13, 14, 7qustgpopn 21846 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑐𝐽) → (𝐹𝑐) ∈ 𝐾)
127123, 124, 125, 126syl3anc 1323 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑐) ∈ 𝐾)
128 simprlr 802 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑑𝐽)
1291, 5, 13, 14, 7qustgpopn 21846 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑑𝐽) → (𝐹𝑑) ∈ 𝐾)
130123, 124, 128, 129syl3anc 1323 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑑) ∈ 𝐾)
13159adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑎𝑋)
132 eceq1 7734 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑎 → [𝑥](𝐺 ~QG 𝑌) = [𝑎](𝐺 ~QG 𝑌))
133132, 7, 79fvmpt3i 6249 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎𝑋 → (𝐹𝑎) = [𝑎](𝐺 ~QG 𝑌))
134131, 133syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑎) = [𝑎](𝐺 ~QG 𝑌))
135123, 16syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝐽 ∈ (TopOn‘𝑋))
136 toponss 20653 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑐𝐽) → 𝑐𝑋)
137135, 125, 136syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑐𝑋)
138 simprrl 803 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝑎𝑐𝑏𝑑))
139138simpld 475 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑎𝑐)
140 fnfvima 6456 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 Fn 𝑋𝑐𝑋𝑎𝑐) → (𝐹𝑎) ∈ (𝐹𝑐))
14180, 140mp3an1 1408 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑐𝑋𝑎𝑐) → (𝐹𝑎) ∈ (𝐹𝑐))
142137, 139, 141syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑎) ∈ (𝐹𝑐))
143134, 142eqeltrrd 2699 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → [𝑎](𝐺 ~QG 𝑌) ∈ (𝐹𝑐))
14460adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑏𝑋)
145 eceq1 7734 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑏 → [𝑥](𝐺 ~QG 𝑌) = [𝑏](𝐺 ~QG 𝑌))
146145, 7, 79fvmpt3i 6249 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏𝑋 → (𝐹𝑏) = [𝑏](𝐺 ~QG 𝑌))
147144, 146syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑏) = [𝑏](𝐺 ~QG 𝑌))
148 toponss 20653 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑑𝐽) → 𝑑𝑋)
149135, 128, 148syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑑𝑋)
150138simprd 479 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑏𝑑)
151 fnfvima 6456 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 Fn 𝑋𝑑𝑋𝑏𝑑) → (𝐹𝑏) ∈ (𝐹𝑑))
15280, 151mp3an1 1408 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑑𝑋𝑏𝑑) → (𝐹𝑏) ∈ (𝐹𝑑))
153149, 150, 152syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑏) ∈ (𝐹𝑑))
154147, 153eqeltrrd 2699 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → [𝑏](𝐺 ~QG 𝑌) ∈ (𝐹𝑑))
155 opelxpi 5113 . . . . . . . . . . . . . . . . . . . 20 (([𝑎](𝐺 ~QG 𝑌) ∈ (𝐹𝑐) ∧ [𝑏](𝐺 ~QG 𝑌) ∈ (𝐹𝑑)) → ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑)))
156143, 154, 155syl2anc 692 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑)))
157137sselda 3587 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ 𝑝𝑐) → 𝑝𝑋)
158149sselda 3587 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ 𝑞𝑑) → 𝑞𝑋)
159157, 158anim12dan 881 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → (𝑝𝑋𝑞𝑋))
160 eceq1 7734 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑝 → [𝑥](𝐺 ~QG 𝑌) = [𝑝](𝐺 ~QG 𝑌))
161160, 7, 79fvmpt3i 6249 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝𝑋 → (𝐹𝑝) = [𝑝](𝐺 ~QG 𝑌))
162 eceq1 7734 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑞 → [𝑥](𝐺 ~QG 𝑌) = [𝑞](𝐺 ~QG 𝑌))
163162, 7, 79fvmpt3i 6249 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑞𝑋 → (𝐹𝑞) = [𝑞](𝐺 ~QG 𝑌))
164 opeq12 4377 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹𝑝) = [𝑝](𝐺 ~QG 𝑌) ∧ (𝐹𝑞) = [𝑞](𝐺 ~QG 𝑌)) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ = ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩)
165161, 163, 164syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑝𝑋𝑞𝑋) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ = ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩)
166159, 165syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ = ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩)
167124adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → 𝑌 ∈ (NrmSGrp‘𝐺))
1681, 5, 24quseccl 17582 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑝𝑋) → [𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻))
1691, 5, 24quseccl 17582 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑞𝑋) → [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻))
170168, 169anim12dan 881 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝑝𝑋𝑞𝑋)) → ([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)))
171167, 159, 170syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)))
172 opelxpi 5113 . . . . . . . . . . . . . . . . . . . . . . . . 25 (([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)) → ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)))
173171, 172syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)))
1741, 5, 61, 27qussub 17586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑝𝑋𝑞𝑋) → ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
1751743expb 1263 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝑝𝑋𝑞𝑋)) → ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
176167, 159, 175syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
177 oveq12 6619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 = 𝑝𝑤 = 𝑞) → (𝑧(-g𝐺)𝑤) = (𝑝(-g𝐺)𝑞))
178177eceq1d 7735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑧 = 𝑝𝑤 = 𝑞) → [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
179 ecexg 7698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐺 ~QG 𝑌) ∈ V → [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌) ∈ V)
1808, 179ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌) ∈ V
181178, 67, 180ovmpt2a 6751 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑝𝑋𝑞𝑋) → (𝑝 𝑞) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
182159, 181syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → (𝑝 𝑞) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
183176, 182eqtr4d 2658 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = (𝑝 𝑞))
184 df-ov 6613 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = ((-g𝐻)‘⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩)
185 df-ov 6613 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 𝑞) = ( ‘⟨𝑝, 𝑞⟩)
186183, 184, 1853eqtr3g 2678 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ((-g𝐻)‘⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩) = ( ‘⟨𝑝, 𝑞⟩))
187 opelxpi 5113 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑝𝑐𝑞𝑑) → ⟨𝑝, 𝑞⟩ ∈ (𝑐 × 𝑑))
188 simprrr 804 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝑐 × 𝑑) ⊆ ( 𝑢))
189188sselda 3587 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ ⟨𝑝, 𝑞⟩ ∈ (𝑐 × 𝑑)) → ⟨𝑝, 𝑞⟩ ∈ ( 𝑢))
190187, 189sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨𝑝, 𝑞⟩ ∈ ( 𝑢))
191 elpreima 6298 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( Fn (𝑋 × 𝑋) → (⟨𝑝, 𝑞⟩ ∈ ( 𝑢) ↔ (⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑝, 𝑞⟩) ∈ 𝑢)))
19299, 191ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟨𝑝, 𝑞⟩ ∈ ( 𝑢) ↔ (⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑝, 𝑞⟩) ∈ 𝑢))
193192simprbi 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑝, 𝑞⟩ ∈ ( 𝑢) → ( ‘⟨𝑝, 𝑞⟩) ∈ 𝑢)
194190, 193syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ( ‘⟨𝑝, 𝑞⟩) ∈ 𝑢)
195186, 194eqeltrd 2698 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ((-g𝐻)‘⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩) ∈ 𝑢)
19653, 54syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (-g𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)))
197196ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → (-g𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)))
198 elpreima 6298 . . . . . . . . . . . . . . . . . . . . . . . . 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 956 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢))
201166, 200eqeltrd 2698 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢))
202201ralrimivva 2966 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ∀𝑝𝑐𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢))
203 opeq1 4375 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = (𝐹𝑝) → ⟨𝑧, 𝑤⟩ = ⟨(𝐹𝑝), 𝑤⟩)
204203eleq1d 2683 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = (𝐹𝑝) → (⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
205204ralbidv 2981 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (𝐹𝑝) → (∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
206205ralima 6458 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 Fn 𝑋𝑐𝑋) → (∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
20780, 206mpan 705 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐𝑋 → (∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
208 opeq2 4376 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = (𝐹𝑞) → ⟨(𝐹𝑝), 𝑤⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩)
209208eleq1d 2683 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = (𝐹𝑞) → (⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
210209ralima 6458 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 Fn 𝑋𝑑𝑋) → (∀𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
21180, 210mpan 705 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑𝑋 → (∀𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
212211ralbidv 2981 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑𝑋 → (∀𝑝𝑐𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
213207, 212sylan9bb 735 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑐𝑋𝑑𝑋) → (∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
214137, 149, 213syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
215202, 214mpbird 247 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢))
216 dfss3 3577 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢) ↔ ∀𝑦 ∈ ((𝐹𝑐) × (𝐹𝑑))𝑦 ∈ ((-g𝐻) “ 𝑢))
217 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = ⟨𝑧, 𝑤⟩ → (𝑦 ∈ ((-g𝐻) “ 𝑢) ↔ ⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
218217ralxp 5228 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦 ∈ ((𝐹𝑐) × (𝐹𝑑))𝑦 ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢))
219216, 218bitri 264 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢) ↔ ∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢))
220215, 219sylibr 224 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢))
221 xpeq1 5093 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟 = (𝐹𝑐) → (𝑟 × 𝑠) = ((𝐹𝑐) × 𝑠))
222221eleq2d 2684 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = (𝐹𝑐) → (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × 𝑠)))
223221sseq1d 3616 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = (𝐹𝑐) → ((𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢) ↔ ((𝐹𝑐) × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
224222, 223anbi12d 746 . . . . . . . . . . . . . . . . . . . 20 (𝑟 = (𝐹𝑐) → ((⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × 𝑠) ∧ ((𝐹𝑐) × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
225 xpeq2 5094 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝐹𝑑) → ((𝐹𝑐) × 𝑠) = ((𝐹𝑐) × (𝐹𝑑)))
226225eleq2d 2684 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝐹𝑑) → (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × 𝑠) ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑))))
227225sseq1d 3616 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝐹𝑑) → (((𝐹𝑐) × 𝑠) ⊆ ((-g𝐻) “ 𝑢) ↔ ((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢)))
228226, 227anbi12d 746 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = (𝐹𝑑) → ((⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × 𝑠) ∧ ((𝐹𝑐) × 𝑠) ⊆ ((-g𝐻) “ 𝑢)) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑)) ∧ ((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢))))
229224, 228rspc2ev 3312 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑐) ∈ 𝐾 ∧ (𝐹𝑑) ∈ 𝐾 ∧ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑)) ∧ ((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢))) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
230127, 130, 156, 220, 229syl112anc 1327 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
231230expr 642 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑐𝐽𝑑𝐽)) → (((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
232231rexlimdvva 3032 . . . . . . . . . . . . . . . 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 483 . . . . . . . . . . . . 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 4377 . . . . . . . . . . . . . 14 ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → ⟨𝑥, 𝑦⟩ = ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩)
238237eleq1d 2683 . . . . . . . . . . . . 13 ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢)))
239237eleq1d 2683 . . . . . . . . . . . . . 14 ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))} ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))}))
240 opex 4898 . . . . . . . . . . . . . . 15 ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ V
241 eleq1 2686 . . . . . . . . . . . . . . . . 17 (𝑤 = ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ → (𝑤 ∈ (𝑟 × 𝑠) ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠)))
242241anbi1d 740 . . . . . . . . . . . . . . . 16 (𝑤 = ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ → ((𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
2432422rexbidv 3051 . . . . . . . . . . . . . . 15 (𝑤 = ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ → (∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)) ↔ ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
244240, 243elab 3337 . . . . . . . . . . . . . 14 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))} ↔ ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
245239, 244syl6bb 276 . . . . . . . . . . . . 13 ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))} ↔ ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
246238, 245imbi12d 334 . . . . . . . . . . . 12 ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → ((⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) → ⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))}) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))))
247236, 246syl5ibrcom 237 . . . . . . . . . . 11 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) → ⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))})))
248247rexlimdvva 3032 . . . . . . . . . 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 5178 . . . . . 6 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ((-g𝐻) “ 𝑢) ⊆ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))})
253 ssabral 3657 . . . . . 6 (((-g𝐻) “ 𝑢) ⊆ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))} ↔ ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
254252, 253sylib 208 . . . . 5 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
255 eltx 21294 . . . . . . 7 ((𝐾 ∈ (TopOn‘(Base‘𝐻)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → (((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
25623, 23, 255syl2anc 692 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
257256adantr 481 . . . . 5 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
258254, 257mpbird 247 . . . 4 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾))
259258ralrimiva 2961 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ∀𝑢𝐾 ((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾))
260 txtopon 21317 . . . . 5 ((𝐾 ∈ (TopOn‘(Base‘𝐻)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → (𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻))))
26123, 23, 260syl2anc 692 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻))))
262 iscn 20962 . . . 4 (((𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻))) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → ((-g𝐻) ∈ ((𝐾 ×t 𝐾) Cn 𝐾) ↔ ((-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) ∧ ∀𝑢𝐾 ((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾))))
263261, 23, 262syl2anc 692 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ((-g𝐻) ∈ ((𝐾 ×t 𝐾) Cn 𝐾) ↔ ((-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) ∧ ∀𝑢𝐾 ((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾))))
26429, 259, 263mpbir2and 956 . 2 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐻) ∈ ((𝐾 ×t 𝐾) Cn 𝐾))
26514, 27istgp2 21818 . 2 (𝐻 ∈ TopGrp ↔ (𝐻 ∈ Grp ∧ 𝐻 ∈ TopSp ∧ (-g𝐻) ∈ ((𝐾 ×t 𝐾) Cn 𝐾)))
2663, 26, 264, 265syl3anbrc 1244 1 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopGrp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  {cab 2607  wral 2907  wrex 2908  Vcvv 3189  wss 3559  cop 4159  cmpt 4678   × cxp 5077  ccnv 5078  dom cdm 5079  cima 5082  Rel wrel 5084   Fn wfn 5847  wf 5848  ontowfo 5850  cfv 5852  (class class class)co 6610  cmpt2 6612  [cec 7692   / cqs 7693  Basecbs 15792  TopOpenctopn 16014   qTop cqtop 16095   /s cqus 16097  Grpcgrp 17354  -gcsg 17356  NrmSGrpcnsg 17521   ~QG cqg 17522  TopOnctopon 20647  TopSpctps 20660   Cn ccn 20951   ×t ctx 21286  TopGrpctgp 21798
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9944  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-mulcom 9952  ax-addass 9953  ax-mulass 9954  ax-distr 9955  ax-i2m1 9956  ax-1ne0 9957  ax-1rid 9958  ax-rnegex 9959  ax-rrecex 9960  ax-cnre 9961  ax-pre-lttri 9962  ax-pre-lttrn 9963  ax-pre-ltadd 9964  ax-pre-mulgt0 9965
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-tpos 7304  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-er 7694  df-ec 7696  df-qs 7700  df-map 7811  df-en 7908  df-dom 7909  df-sdom 7910  df-fin 7911  df-sup 8300  df-inf 8301  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-sub 10220  df-neg 10221  df-nn 10973  df-2 11031  df-3 11032  df-4 11033  df-5 11034  df-6 11035  df-7 11036  df-8 11037  df-9 11038  df-n0 11245  df-z 11330  df-dec 11446  df-uz 11640  df-fz 12277  df-struct 15794  df-ndx 15795  df-slot 15796  df-base 15797  df-sets 15798  df-ress 15799  df-plusg 15886  df-mulr 15887  df-sca 15889  df-vsca 15890  df-ip 15891  df-tset 15892  df-ple 15893  df-ds 15896  df-rest 16015  df-topn 16016  df-0g 16034  df-topgen 16036  df-qtop 16099  df-imas 16100  df-qus 16101  df-plusf 17173  df-mgm 17174  df-sgrp 17216  df-mnd 17227  df-grp 17357  df-minusg 17358  df-sbg 17359  df-subg 17523  df-nsg 17524  df-eqg 17525  df-oppg 17708  df-top 20631  df-topon 20648  df-topsp 20661  df-bases 20674  df-cn 20954  df-cnp 20955  df-tx 21288  df-hmeo 21481  df-tmd 21799  df-tgp 21800
This theorem is referenced by:  qustgp  21848
  Copyright terms: Public domain W3C validator