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

Theorem qustgplem 22145
Description: Lemma for qustgp 22146. (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 17858 . . 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 6824 . . . . . . . 8 (𝐺 ~QG 𝑌) ∈ V
98a1i 11 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐺 ~QG 𝑌) ∈ V)
10 simpl 468 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐺 ∈ TopGrp)
114, 6, 7, 9, 10qusval 16411 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 = (𝐹s 𝐺))
124, 6, 7, 9, 10quslem 16412 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹:𝑋onto→(𝑋 / (𝐺 ~QG 𝑌)))
13 qustgpopn.j . . . . . 6 𝐽 = (TopOpen‘𝐺)
14 qustgpopn.k . . . . . 6 𝐾 = (TopOpen‘𝐻)
1511, 6, 12, 10, 13, 14imastopn 21745 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 = (𝐽 qTop 𝐹))
1613, 5tgptopon 22107 . . . . . . 7 (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋))
1716adantr 466 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐽 ∈ (TopOn‘𝑋))
18 qtoptopon 21729 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto→(𝑋 / (𝐺 ~QG 𝑌))) → (𝐽 qTop 𝐹) ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))))
1917, 12, 18syl2anc 567 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐽 qTop 𝐹) ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))))
2015, 19eqeltrd 2850 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))))
214, 6, 9, 10qusbas 16414 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑋 / (𝐺 ~QG 𝑌)) = (Base‘𝐻))
2221fveq2d 6337 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))) = (TopOn‘(Base‘𝐻)))
2320, 22eleqtrd 2852 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 ∈ (TopOn‘(Base‘𝐻)))
24 eqid 2771 . . . 4 (Base‘𝐻) = (Base‘𝐻)
2524, 14istps 20960 . . 3 (𝐻 ∈ TopSp ↔ 𝐾 ∈ (TopOn‘(Base‘𝐻)))
2623, 25sylibr 224 . 2 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopSp)
27 eqid 2771 . . . . 5 (-g𝐻) = (-g𝐻)
2824, 27grpsubf 17703 . . . 4 (𝐻 ∈ Grp → (-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻))
293, 28syl 17 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻))
30 cnvimass 5627 . . . . . . . . 9 ((-g𝐻) “ 𝑢) ⊆ dom (-g𝐻)
31 fdm 6192 . . . . . . . . . . 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 3803 . . . . . . . 8 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ((-g𝐻) “ 𝑢) ⊆ ((Base‘𝐻) × (Base‘𝐻)))
35 relxp 5267 . . . . . . . 8 Rel ((Base‘𝐻) × (Base‘𝐻))
36 relss 5347 . . . . . . . 8 (((-g𝐻) “ 𝑢) ⊆ ((Base‘𝐻) × (Base‘𝐻)) → (Rel ((Base‘𝐻) × (Base‘𝐻)) → Rel ((-g𝐻) “ 𝑢)))
3734, 35, 36mpisyl 21 . . . . . . 7 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → Rel ((-g𝐻) “ 𝑢))
3834sseld 3752 . . . . . . . 8 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐻) × (Base‘𝐻))))
39 vex 3354 . . . . . . . . . . . . . 14 𝑥 ∈ V
4039elqs 7952 . . . . . . . . . . . . 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 7952 . . . . . . . . . . . . 13 (𝑦 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ ∃𝑏𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌))
4641eleq2d 2836 . . . . . . . . . . . . 13 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (𝑦 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ 𝑦 ∈ (Base‘𝐻)))
4745, 46syl5bbr 274 . . . . . . . . . . . 12 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (∃𝑏𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌) ↔ 𝑦 ∈ (Base‘𝐻)))
4843, 47anbi12d 610 . . . . . . . . . . 11 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ((∃𝑎𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ ∃𝑏𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))))
49 reeanv 3255 . . . . . . . . . . 11 (∃𝑎𝑋𝑏𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ (∃𝑎𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ ∃𝑏𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌)))
50 opelxp 5287 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻)))
5148, 49, 503bitr4g 303 . . . . . . . . . 10 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (∃𝑎𝑋𝑏𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐻) × (Base‘𝐻))))
523ad2antrr 699 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝐻 ∈ Grp)
5352, 28syl 17 . . . . . . . . . . . . . 14 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻))
54 ffn 6186 . . . . . . . . . . . . . 14 ((-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) → (-g𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)))
55 elpreima 6481 . . . . . . . . . . . . . 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 6797 . . . . . . . . . . . . . . . . 17 ([𝑎](𝐺 ~QG 𝑌)(-g𝐻)[𝑏](𝐺 ~QG 𝑌)) = ((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩)
58 simpllr 754 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝑌 ∈ (NrmSGrp‘𝐺))
59 simprl 748 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝑎𝑋)
60 simprr 750 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝑏𝑋)
61 eqid 2771 . . . . . . . . . . . . . . . . . . 19 (-g𝐺) = (-g𝐺)
621, 5, 61, 27qussub 17863 . . . . . . . . . . . . . . . . . 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 22103 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
6968adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐺 ∈ Grp)
705, 61grpsubf 17703 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐺 ∈ Grp → (-g𝐺):(𝑋 × 𝑋)⟶𝑋)
71 ffn 6186 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((-g𝐺):(𝑋 × 𝑋)⟶𝑋 → (-g𝐺) Fn (𝑋 × 𝑋))
7269, 70, 713syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐺) Fn (𝑋 × 𝑋))
73 fnov 6916 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((-g𝐺) Fn (𝑋 × 𝑋) ↔ (-g𝐺) = (𝑧𝑋, 𝑤𝑋 ↦ (𝑧(-g𝐺)𝑤)))
7472, 73sylib 208 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐺) = (𝑧𝑋, 𝑤𝑋 ↦ (𝑧(-g𝐺)𝑤)))
7513, 61tgpsubcn 22115 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐺 ∈ TopGrp → (-g𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
7675adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
7774, 76eqeltrrd 2851 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑧𝑋, 𝑤𝑋 ↦ (𝑧(-g𝐺)𝑤)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
78 ecexg 7901 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐺 ~QG 𝑌) ∈ V → [𝑥](𝐺 ~QG 𝑌) ∈ V)
798, 78ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 [𝑥](𝐺 ~QG 𝑌) ∈ V
8079, 7fnmpti 6163 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝐹 Fn 𝑋
81 qtopid 21730 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 Fn 𝑋) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)))
8217, 80, 81sylancl 568 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)))
8315oveq2d 6810 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐽 Cn 𝐾) = (𝐽 Cn (𝐽 qTop 𝐹)))
8482, 83eleqtrrd 2853 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹 ∈ (𝐽 Cn 𝐾))
857, 84syl5eqelr 2855 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑥𝑋 ↦ [𝑥](𝐺 ~QG 𝑌)) ∈ (𝐽 Cn 𝐾))
86 eceq1 7935 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑧(-g𝐺)𝑤) → [𝑥](𝐺 ~QG 𝑌) = [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌))
8717, 17, 77, 17, 85, 86cnmpt21 21696 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑧𝑋, 𝑤𝑋 ↦ [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌)) ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
8867, 87syl5eqel 2854 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
8988ad2antrr 699 . . . . . . . . . . . . . . . . . . . 20 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
90 simplr 746 . . . . . . . . . . . . . . . . . . . 20 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝑢𝐾)
91 cnima 21291 . . . . . . . . . . . . . . . . . . . 20 (( ∈ ((𝐽 ×t 𝐽) Cn 𝐾) ∧ 𝑢𝐾) → ( 𝑢) ∈ (𝐽 ×t 𝐽))
9289, 90, 91syl2anc 567 . . . . . . . . . . . . . . . . . . 19 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ( 𝑢) ∈ (𝐽 ×t 𝐽))
9317ad2antrr 699 . . . . . . . . . . . . . . . . . . . 20 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
94 eltx 21593 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘𝑋)) → (( 𝑢) ∈ (𝐽 ×t 𝐽) ↔ ∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
9593, 93, 94syl2anc 567 . . . . . . . . . . . . . . . . . . 19 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (( 𝑢) ∈ (𝐽 ×t 𝐽) ↔ ∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
9692, 95mpbid 222 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))
97 ecexg 7901 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ~QG 𝑌) ∈ V → [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌) ∈ V)
988, 97ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌) ∈ V
9967, 98fnmpt2i 7390 . . . . . . . . . . . . . . . . . . . . 21 Fn (𝑋 × 𝑋)
100 elpreima 6481 . . . . . . . . . . . . . . . . . . . . 21 ( Fn (𝑋 × 𝑋) → (⟨𝑎, 𝑏⟩ ∈ ( 𝑢) ↔ (⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢)))
10199, 100ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑎, 𝑏⟩ ∈ ( 𝑢) ↔ (⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢))
102 opelxp 5287 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋) ↔ (𝑎𝑋𝑏𝑋))
103102anbi1i 604 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢) ↔ ((𝑎𝑋𝑏𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢))
104 df-ov 6797 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 𝑏) = ( ‘⟨𝑎, 𝑏⟩)
105 oveq12 6803 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑧 = 𝑎𝑤 = 𝑏) → (𝑧(-g𝐺)𝑤) = (𝑎(-g𝐺)𝑏))
106105eceq1d 7936 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 = 𝑎𝑤 = 𝑏) → [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
107 ecexg 7901 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ~QG 𝑌) ∈ V → [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ V)
1088, 107ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ V
109106, 67, 108ovmpt2a 6939 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝑋𝑏𝑋) → (𝑎 𝑏) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
110104, 109syl5eqr 2819 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎𝑋𝑏𝑋) → ( ‘⟨𝑎, 𝑏⟩) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
111110eleq1d 2835 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎𝑋𝑏𝑋) → (( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢 ↔ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢))
112111pm5.32i 558 . . . . . . . . . . . . . . . . . . . 20 (((𝑎𝑋𝑏𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢) ↔ ((𝑎𝑋𝑏𝑋) ∧ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢))
113101, 103, 1123bitri 286 . . . . . . . . . . . . . . . . . . 19 (⟨𝑎, 𝑏⟩ ∈ ( 𝑢) ↔ ((𝑎𝑋𝑏𝑋) ∧ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢))
114 eleq1 2838 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑡 ∈ (𝑐 × 𝑑) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑)))
115 opelxp 5287 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ↔ (𝑎𝑐𝑏𝑑))
116114, 115syl6bb 276 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑡 ∈ (𝑐 × 𝑑) ↔ (𝑎𝑐𝑏𝑑)))
117116anbi1d 609 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) ↔ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
1181172rexbidv 3205 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = ⟨𝑎, 𝑏⟩ → (∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) ↔ ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
119118rspccv 3458 . . . . . . . . . . . . . . . . . . 19 (∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) → (⟨𝑎, 𝑏⟩ ∈ ( 𝑢) → ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
120113, 119syl5bir 233 . . . . . . . . . . . . . . . . . 18 (∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) → (((𝑎𝑋𝑏𝑋) ∧ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢) → ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
12196, 120syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (((𝑎𝑋𝑏𝑋) ∧ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢) → ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
12266, 121mpand 669 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ([(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢 → ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
123 simp-4l 762 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝐺 ∈ TopGrp)
12458adantr 466 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑌 ∈ (NrmSGrp‘𝐺))
125 simprll 758 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑐𝐽)
1261, 5, 13, 14, 7qustgpopn 22144 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑐𝐽) → (𝐹𝑐) ∈ 𝐾)
127123, 124, 125, 126syl3anc 1476 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑐) ∈ 𝐾)
128 simprlr 759 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑑𝐽)
1291, 5, 13, 14, 7qustgpopn 22144 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑑𝐽) → (𝐹𝑑) ∈ 𝐾)
130123, 124, 128, 129syl3anc 1476 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑑) ∈ 𝐾)
13159adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑎𝑋)
132 eceq1 7935 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑎 → [𝑥](𝐺 ~QG 𝑌) = [𝑎](𝐺 ~QG 𝑌))
133132, 7, 79fvmpt3i 6430 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎𝑋 → (𝐹𝑎) = [𝑎](𝐺 ~QG 𝑌))
134131, 133syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑎) = [𝑎](𝐺 ~QG 𝑌))
135123, 16syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝐽 ∈ (TopOn‘𝑋))
136 toponss 20953 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑐𝐽) → 𝑐𝑋)
137135, 125, 136syl2anc 567 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑐𝑋)
138 simprrl 760 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝑎𝑐𝑏𝑑))
139138simpld 478 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑎𝑐)
140 fnfvima 6640 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 Fn 𝑋𝑐𝑋𝑎𝑐) → (𝐹𝑎) ∈ (𝐹𝑐))
14180, 140mp3an1 1559 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑐𝑋𝑎𝑐) → (𝐹𝑎) ∈ (𝐹𝑐))
142137, 139, 141syl2anc 567 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑎) ∈ (𝐹𝑐))
143134, 142eqeltrrd 2851 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → [𝑎](𝐺 ~QG 𝑌) ∈ (𝐹𝑐))
14460adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑏𝑋)
145 eceq1 7935 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑏 → [𝑥](𝐺 ~QG 𝑌) = [𝑏](𝐺 ~QG 𝑌))
146145, 7, 79fvmpt3i 6430 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏𝑋 → (𝐹𝑏) = [𝑏](𝐺 ~QG 𝑌))
147144, 146syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑏) = [𝑏](𝐺 ~QG 𝑌))
148 toponss 20953 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑑𝐽) → 𝑑𝑋)
149135, 128, 148syl2anc 567 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑑𝑋)
150138simprd 479 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑏𝑑)
151 fnfvima 6640 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 Fn 𝑋𝑑𝑋𝑏𝑑) → (𝐹𝑏) ∈ (𝐹𝑑))
15280, 151mp3an1 1559 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑑𝑋𝑏𝑑) → (𝐹𝑏) ∈ (𝐹𝑑))
153149, 150, 152syl2anc 567 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑏) ∈ (𝐹𝑑))
154147, 153eqeltrrd 2851 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → [𝑏](𝐺 ~QG 𝑌) ∈ (𝐹𝑑))
155 opelxpi 5289 . . . . . . . . . . . . . . . . . . . 20 (([𝑎](𝐺 ~QG 𝑌) ∈ (𝐹𝑐) ∧ [𝑏](𝐺 ~QG 𝑌) ∈ (𝐹𝑑)) → ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑)))
156143, 154, 155syl2anc 567 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑)))
157137sselda 3753 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ 𝑝𝑐) → 𝑝𝑋)
158149sselda 3753 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ 𝑞𝑑) → 𝑞𝑋)
159157, 158anim12dan 599 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → (𝑝𝑋𝑞𝑋))
160 eceq1 7935 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑝 → [𝑥](𝐺 ~QG 𝑌) = [𝑝](𝐺 ~QG 𝑌))
161160, 7, 79fvmpt3i 6430 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝𝑋 → (𝐹𝑝) = [𝑝](𝐺 ~QG 𝑌))
162 eceq1 7935 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑞 → [𝑥](𝐺 ~QG 𝑌) = [𝑞](𝐺 ~QG 𝑌))
163162, 7, 79fvmpt3i 6430 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑞𝑋 → (𝐹𝑞) = [𝑞](𝐺 ~QG 𝑌))
164 opeq12 4542 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹𝑝) = [𝑝](𝐺 ~QG 𝑌) ∧ (𝐹𝑞) = [𝑞](𝐺 ~QG 𝑌)) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ = ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩)
165161, 163, 164syl2an 577 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑝𝑋𝑞𝑋) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ = ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩)
166159, 165syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ = ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩)
167124adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → 𝑌 ∈ (NrmSGrp‘𝐺))
1681, 5, 24quseccl 17859 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑝𝑋) → [𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻))
1691, 5, 24quseccl 17859 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑞𝑋) → [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻))
170168, 169anim12dan 599 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝑝𝑋𝑞𝑋)) → ([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)))
171167, 159, 170syl2anc 567 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)))
172 opelxpi 5289 . . . . . . . . . . . . . . . . . . . . . . . . 25 (([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)) → ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)))
173171, 172syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)))
1741, 5, 61, 27qussub 17863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑝𝑋𝑞𝑋) → ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
1751743expb 1113 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝑝𝑋𝑞𝑋)) → ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
176167, 159, 175syl2anc 567 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
177 oveq12 6803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 = 𝑝𝑤 = 𝑞) → (𝑧(-g𝐺)𝑤) = (𝑝(-g𝐺)𝑞))
178177eceq1d 7936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑧 = 𝑝𝑤 = 𝑞) → [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
179 ecexg 7901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐺 ~QG 𝑌) ∈ V → [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌) ∈ V)
1808, 179ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌) ∈ V
181178, 67, 180ovmpt2a 6939 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑝𝑋𝑞𝑋) → (𝑝 𝑞) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
182159, 181syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → (𝑝 𝑞) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
183176, 182eqtr4d 2808 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = (𝑝 𝑞))
184 df-ov 6797 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = ((-g𝐻)‘⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩)
185 df-ov 6797 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 𝑞) = ( ‘⟨𝑝, 𝑞⟩)
186183, 184, 1853eqtr3g 2828 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ((-g𝐻)‘⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩) = ( ‘⟨𝑝, 𝑞⟩))
187 opelxpi 5289 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑝𝑐𝑞𝑑) → ⟨𝑝, 𝑞⟩ ∈ (𝑐 × 𝑑))
188 simprrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝑐 × 𝑑) ⊆ ( 𝑢))
189188sselda 3753 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ ⟨𝑝, 𝑞⟩ ∈ (𝑐 × 𝑑)) → ⟨𝑝, 𝑞⟩ ∈ ( 𝑢))
190187, 189sylan2 574 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨𝑝, 𝑞⟩ ∈ ( 𝑢))
191 elpreima 6481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( Fn (𝑋 × 𝑋) → (⟨𝑝, 𝑞⟩ ∈ ( 𝑢) ↔ (⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑝, 𝑞⟩) ∈ 𝑢)))
19299, 191ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟨𝑝, 𝑞⟩ ∈ ( 𝑢) ↔ (⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑝, 𝑞⟩) ∈ 𝑢))
193192simprbi 480 . . . . . . . . . . . . . . . . . . . . . . . . . 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 699 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → (-g𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)))
198 elpreima 6481 . . . . . . . . . . . . . . . . . . . . . . . . 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 686 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢))
201166, 200eqeltrd 2850 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢))
202201ralrimivva 3120 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ∀𝑝𝑐𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢))
203 opeq1 4540 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = (𝐹𝑝) → ⟨𝑧, 𝑤⟩ = ⟨(𝐹𝑝), 𝑤⟩)
204203eleq1d 2835 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = (𝐹𝑝) → (⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
205204ralbidv 3135 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (𝐹𝑝) → (∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
206205ralima 6642 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 Fn 𝑋𝑐𝑋) → (∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
20780, 206mpan 664 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐𝑋 → (∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
208 opeq2 4541 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = (𝐹𝑞) → ⟨(𝐹𝑝), 𝑤⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩)
209208eleq1d 2835 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = (𝐹𝑞) → (⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
210209ralima 6642 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 Fn 𝑋𝑑𝑋) → (∀𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
21180, 210mpan 664 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑𝑋 → (∀𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
212211ralbidv 3135 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑𝑋 → (∀𝑝𝑐𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
213207, 212sylan9bb 495 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑐𝑋𝑑𝑋) → (∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
214137, 149, 213syl2anc 567 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
215202, 214mpbird 247 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢))
216 dfss3 3742 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢) ↔ ∀𝑦 ∈ ((𝐹𝑐) × (𝐹𝑑))𝑦 ∈ ((-g𝐻) “ 𝑢))
217 eleq1 2838 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = ⟨𝑧, 𝑤⟩ → (𝑦 ∈ ((-g𝐻) “ 𝑢) ↔ ⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
218217ralxp 5403 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦 ∈ ((𝐹𝑐) × (𝐹𝑑))𝑦 ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢))
219216, 218bitri 264 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢) ↔ ∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢))
220215, 219sylibr 224 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢))
221 xpeq1 5264 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟 = (𝐹𝑐) → (𝑟 × 𝑠) = ((𝐹𝑐) × 𝑠))
222221eleq2d 2836 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = (𝐹𝑐) → (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × 𝑠)))
223221sseq1d 3782 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = (𝐹𝑐) → ((𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢) ↔ ((𝐹𝑐) × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
224222, 223anbi12d 610 . . . . . . . . . . . . . . . . . . . 20 (𝑟 = (𝐹𝑐) → ((⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × 𝑠) ∧ ((𝐹𝑐) × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
225 xpeq2 5270 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝐹𝑑) → ((𝐹𝑐) × 𝑠) = ((𝐹𝑐) × (𝐹𝑑)))
226225eleq2d 2836 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝐹𝑑) → (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × 𝑠) ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑))))
227225sseq1d 3782 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝐹𝑑) → (((𝐹𝑐) × 𝑠) ⊆ ((-g𝐻) “ 𝑢) ↔ ((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢)))
228226, 227anbi12d 610 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = (𝐹𝑑) → ((⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × 𝑠) ∧ ((𝐹𝑐) × 𝑠) ⊆ ((-g𝐻) “ 𝑢)) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑)) ∧ ((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢))))
229224, 228rspc2ev 3475 . . . . . . . . . . . . . . . . . . 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 474 . . . . . . . . . . . . 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 4542 . . . . . . . . . . . . . 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 5061 . . . . . . . . . . . . . . 15 ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ V
241 eleq1 2838 . . . . . . . . . . . . . . . . 17 (𝑤 = ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ → (𝑤 ∈ (𝑟 × 𝑠) ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠)))
242241anbi1d 609 . . . . . . . . . . . . . . . 16 (𝑤 = ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ → ((𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
2432422rexbidv 3205 . . . . . . . . . . . . . . 15 (𝑤 = ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ → (∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)) ↔ ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
244240, 243elab 3502 . . . . . . . . . . . . . 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 5353 . . . . . 6 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ((-g𝐻) “ 𝑢) ⊆ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))})
253 ssabral 3823 . . . . . 6 (((-g𝐻) “ 𝑢) ⊆ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))} ↔ ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
254252, 253sylib 208 . . . . 5 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
255 eltx 21593 . . . . . . 7 ((𝐾 ∈ (TopOn‘(Base‘𝐻)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → (((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
25623, 23, 255syl2anc 567 . . . . . 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 21616 . . . . 5 ((𝐾 ∈ (TopOn‘(Base‘𝐻)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → (𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻))))
26123, 23, 260syl2anc 567 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻))))
262 iscn 21261 . . . 4 (((𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻))) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → ((-g𝐻) ∈ ((𝐾 ×t 𝐾) Cn 𝐾) ↔ ((-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) ∧ ∀𝑢𝐾 ((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾))))
263261, 23, 262syl2anc 567 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ((-g𝐻) ∈ ((𝐾 ×t 𝐾) Cn 𝐾) ↔ ((-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) ∧ ∀𝑢𝐾 ((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾))))
26429, 259, 263mpbir2and 686 . 2 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐻) ∈ ((𝐾 ×t 𝐾) Cn 𝐾))
26514, 27istgp2 22116 . 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 3724  cop 4323  cmpt 4864   × cxp 5248  ccnv 5249  dom cdm 5250  cima 5253  Rel wrel 5255   Fn wfn 6027  wf 6028  ontowfo 6030  cfv 6032  (class class class)co 6794  cmpt2 6796  [cec 7895   / cqs 7896  Basecbs 16065  TopOpenctopn 16291   qTop cqtop 16372   /s cqus 16374  Grpcgrp 17631  -gcsg 17633  NrmSGrpcnsg 17798   ~QG cqg 17799  TopOnctopon 20936  TopSpctps 20958   Cn ccn 21250   ×t ctx 21585  TopGrpctgp 22096
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 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097  ax-cnex 10195  ax-resscn 10196  ax-1cn 10197  ax-icn 10198  ax-addcl 10199  ax-addrcl 10200  ax-mulcl 10201  ax-mulrcl 10202  ax-mulcom 10203  ax-addass 10204  ax-mulass 10205  ax-distr 10206  ax-i2m1 10207  ax-1ne0 10208  ax-1rid 10209  ax-rnegex 10210  ax-rrecex 10211  ax-cnre 10212  ax-pre-lttri 10213  ax-pre-lttrn 10214  ax-pre-ltadd 10215  ax-pre-mulgt0 10216
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  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 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5824  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-riota 6755  df-ov 6797  df-oprab 6798  df-mpt2 6799  df-om 7214  df-1st 7316  df-2nd 7317  df-tpos 7505  df-wrecs 7560  df-recs 7622  df-rdg 7660  df-1o 7714  df-oadd 7718  df-er 7897  df-ec 7899  df-qs 7903  df-map 8012  df-en 8111  df-dom 8112  df-sdom 8113  df-fin 8114  df-sup 8505  df-inf 8506  df-pnf 10279  df-mnf 10280  df-xr 10281  df-ltxr 10282  df-le 10283  df-sub 10471  df-neg 10472  df-nn 11224  df-2 11282  df-3 11283  df-4 11284  df-5 11285  df-6 11286  df-7 11287  df-8 11288  df-9 11289  df-n0 11496  df-z 11581  df-dec 11697  df-uz 11890  df-fz 12535  df-struct 16067  df-ndx 16068  df-slot 16069  df-base 16071  df-sets 16072  df-ress 16073  df-plusg 16163  df-mulr 16164  df-sca 16166  df-vsca 16167  df-ip 16168  df-tset 16169  df-ple 16170  df-ds 16173  df-rest 16292  df-topn 16293  df-0g 16311  df-topgen 16313  df-qtop 16376  df-imas 16377  df-qus 16378  df-plusf 17450  df-mgm 17451  df-sgrp 17493  df-mnd 17504  df-grp 17634  df-minusg 17635  df-sbg 17636  df-subg 17800  df-nsg 17801  df-eqg 17802  df-oppg 17984  df-top 20920  df-topon 20937  df-topsp 20959  df-bases 20972  df-cn 21253  df-cnp 21254  df-tx 21587  df-hmeo 21780  df-tmd 22097  df-tgp 22098
This theorem is referenced by:  qustgp  22146
  Copyright terms: Public domain W3C validator