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

Theorem qustgplem 23606
Description: Lemma for qustgp 23607. (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 19058 . . 3 (𝑌 ∈ (NrmSGrp‘𝐺) → 𝐻 ∈ Grp)
32adantl 483 . 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 7436 . . . . . . . 8 (𝐺 ~QG 𝑌) ∈ V
98a1i 11 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐺 ~QG 𝑌) ∈ V)
10 simpl 484 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐺 ∈ TopGrp)
114, 6, 7, 9, 10qusval 17483 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 = (𝐹s 𝐺))
124, 6, 7, 9, 10quslem 17484 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹:𝑋onto→(𝑋 / (𝐺 ~QG 𝑌)))
13 qustgpopn.j . . . . . 6 𝐽 = (TopOpen‘𝐺)
14 qustgpopn.k . . . . . 6 𝐾 = (TopOpen‘𝐻)
1511, 6, 12, 10, 13, 14imastopn 23205 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 = (𝐽 qTop 𝐹))
1613, 5tgptopon 23567 . . . . . . 7 (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋))
1716adantr 482 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐽 ∈ (TopOn‘𝑋))
18 qtoptopon 23189 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto→(𝑋 / (𝐺 ~QG 𝑌))) → (𝐽 qTop 𝐹) ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))))
1917, 12, 18syl2anc 585 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐽 qTop 𝐹) ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))))
2015, 19eqeltrd 2834 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))))
214, 6, 9, 10qusbas 17486 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑋 / (𝐺 ~QG 𝑌)) = (Base‘𝐻))
2221fveq2d 6891 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))) = (TopOn‘(Base‘𝐻)))
2320, 22eleqtrd 2836 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 ∈ (TopOn‘(Base‘𝐻)))
24 eqid 2733 . . . 4 (Base‘𝐻) = (Base‘𝐻)
2524, 14istps 22417 . . 3 (𝐻 ∈ TopSp ↔ 𝐾 ∈ (TopOn‘(Base‘𝐻)))
2623, 25sylibr 233 . 2 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopSp)
27 eqid 2733 . . . . 5 (-g𝐻) = (-g𝐻)
2824, 27grpsubf 18897 . . . 4 (𝐻 ∈ Grp → (-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻))
293, 28syl 17 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻))
30 cnvimass 6076 . . . . . . . . 9 ((-g𝐻) “ 𝑢) ⊆ dom (-g𝐻)
3129fdmd 6724 . . . . . . . . . 10 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → dom (-g𝐻) = ((Base‘𝐻) × (Base‘𝐻)))
3231adantr 482 . . . . . . . . 9 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → dom (-g𝐻) = ((Base‘𝐻) × (Base‘𝐻)))
3330, 32sseqtrid 4032 . . . . . . . 8 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ((-g𝐻) “ 𝑢) ⊆ ((Base‘𝐻) × (Base‘𝐻)))
34 relxp 5692 . . . . . . . 8 Rel ((Base‘𝐻) × (Base‘𝐻))
35 relss 5778 . . . . . . . 8 (((-g𝐻) “ 𝑢) ⊆ ((Base‘𝐻) × (Base‘𝐻)) → (Rel ((Base‘𝐻) × (Base‘𝐻)) → Rel ((-g𝐻) “ 𝑢)))
3633, 34, 35mpisyl 21 . . . . . . 7 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → Rel ((-g𝐻) “ 𝑢))
3733sseld 3979 . . . . . . . 8 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐻) × (Base‘𝐻))))
38 vex 3479 . . . . . . . . . . . . . 14 𝑥 ∈ V
3938elqs 8758 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ ∃𝑎𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌))
4021adantr 482 . . . . . . . . . . . . . 14 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (𝑋 / (𝐺 ~QG 𝑌)) = (Base‘𝐻))
4140eleq2d 2820 . . . . . . . . . . . . 13 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (𝑥 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ 𝑥 ∈ (Base‘𝐻)))
4239, 41bitr3id 285 . . . . . . . . . . . 12 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (∃𝑎𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ↔ 𝑥 ∈ (Base‘𝐻)))
43 vex 3479 . . . . . . . . . . . . . 14 𝑦 ∈ V
4443elqs 8758 . . . . . . . . . . . . 13 (𝑦 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ ∃𝑏𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌))
4540eleq2d 2820 . . . . . . . . . . . . 13 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (𝑦 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ 𝑦 ∈ (Base‘𝐻)))
4644, 45bitr3id 285 . . . . . . . . . . . 12 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (∃𝑏𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌) ↔ 𝑦 ∈ (Base‘𝐻)))
4742, 46anbi12d 632 . . . . . . . . . . 11 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ((∃𝑎𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ ∃𝑏𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))))
48 reeanv 3227 . . . . . . . . . . 11 (∃𝑎𝑋𝑏𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ (∃𝑎𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ ∃𝑏𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌)))
49 opelxp 5710 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻)))
5047, 48, 493bitr4g 314 . . . . . . . . . 10 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (∃𝑎𝑋𝑏𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐻) × (Base‘𝐻))))
513ad2antrr 725 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝐻 ∈ Grp)
5251, 28syl 17 . . . . . . . . . . . . . 14 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻))
53 ffn 6713 . . . . . . . . . . . . . 14 ((-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) → (-g𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)))
54 elpreima 7054 . . . . . . . . . . . . . 14 ((-g𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)) → (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧ ((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩) ∈ 𝑢)))
5552, 53, 543syl 18 . . . . . . . . . . . . 13 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧ ((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩) ∈ 𝑢)))
56 df-ov 7406 . . . . . . . . . . . . . . . . 17 ([𝑎](𝐺 ~QG 𝑌)(-g𝐻)[𝑏](𝐺 ~QG 𝑌)) = ((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩)
57 simpllr 775 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝑌 ∈ (NrmSGrp‘𝐺))
58 simprl 770 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝑎𝑋)
59 simprr 772 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝑏𝑋)
60 eqid 2733 . . . . . . . . . . . . . . . . . . 19 (-g𝐺) = (-g𝐺)
611, 5, 60, 27qussub 19063 . . . . . . . . . . . . . . . . . 18 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑎𝑋𝑏𝑋) → ([𝑎](𝐺 ~QG 𝑌)(-g𝐻)[𝑏](𝐺 ~QG 𝑌)) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
6257, 58, 59, 61syl3anc 1372 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ([𝑎](𝐺 ~QG 𝑌)(-g𝐻)[𝑏](𝐺 ~QG 𝑌)) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
6356, 62eqtr3id 2787 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
6463eleq1d 2819 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩) ∈ 𝑢 ↔ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢))
65 simpr 486 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (𝑎𝑋𝑏𝑋))
66 qustgplem.m . . . . . . . . . . . . . . . . . . . . . 22 = (𝑧𝑋, 𝑤𝑋 ↦ [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌))
67 tgpgrp 23563 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
6867adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐺 ∈ Grp)
695, 60grpsubf 18897 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐺 ∈ Grp → (-g𝐺):(𝑋 × 𝑋)⟶𝑋)
70 ffn 6713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((-g𝐺):(𝑋 × 𝑋)⟶𝑋 → (-g𝐺) Fn (𝑋 × 𝑋))
7168, 69, 703syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐺) Fn (𝑋 × 𝑋))
72 fnov 7534 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((-g𝐺) Fn (𝑋 × 𝑋) ↔ (-g𝐺) = (𝑧𝑋, 𝑤𝑋 ↦ (𝑧(-g𝐺)𝑤)))
7371, 72sylib 217 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐺) = (𝑧𝑋, 𝑤𝑋 ↦ (𝑧(-g𝐺)𝑤)))
7413, 60tgpsubcn 23575 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐺 ∈ TopGrp → (-g𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
7574adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
7673, 75eqeltrrd 2835 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑧𝑋, 𝑤𝑋 ↦ (𝑧(-g𝐺)𝑤)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
77 ecexg 8702 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐺 ~QG 𝑌) ∈ V → [𝑥](𝐺 ~QG 𝑌) ∈ V)
788, 77ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 [𝑥](𝐺 ~QG 𝑌) ∈ V
7978, 7fnmpti 6689 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝐹 Fn 𝑋
80 qtopid 23190 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 Fn 𝑋) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)))
8117, 79, 80sylancl 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)))
8215oveq2d 7419 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐽 Cn 𝐾) = (𝐽 Cn (𝐽 qTop 𝐹)))
8381, 82eleqtrrd 2837 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹 ∈ (𝐽 Cn 𝐾))
847, 83eqeltrrid 2839 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑥𝑋 ↦ [𝑥](𝐺 ~QG 𝑌)) ∈ (𝐽 Cn 𝐾))
85 eceq1 8736 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑧(-g𝐺)𝑤) → [𝑥](𝐺 ~QG 𝑌) = [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌))
8617, 17, 76, 17, 84, 85cnmpt21 23156 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑧𝑋, 𝑤𝑋 ↦ [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌)) ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
8766, 86eqeltrid 2838 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
8887ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
89 simplr 768 . . . . . . . . . . . . . . . . . . . 20 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝑢𝐾)
90 cnima 22750 . . . . . . . . . . . . . . . . . . . 20 (( ∈ ((𝐽 ×t 𝐽) Cn 𝐾) ∧ 𝑢𝐾) → ( 𝑢) ∈ (𝐽 ×t 𝐽))
9188, 89, 90syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ( 𝑢) ∈ (𝐽 ×t 𝐽))
9217ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
93 eltx 23053 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘𝑋)) → (( 𝑢) ∈ (𝐽 ×t 𝐽) ↔ ∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
9492, 92, 93syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (( 𝑢) ∈ (𝐽 ×t 𝐽) ↔ ∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
9591, 94mpbid 231 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))
96 ecexg 8702 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ~QG 𝑌) ∈ V → [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌) ∈ V)
978, 96ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌) ∈ V
9866, 97fnmpoi 8050 . . . . . . . . . . . . . . . . . . . . 21 Fn (𝑋 × 𝑋)
99 elpreima 7054 . . . . . . . . . . . . . . . . . . . . 21 ( Fn (𝑋 × 𝑋) → (⟨𝑎, 𝑏⟩ ∈ ( 𝑢) ↔ (⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢)))
10098, 99ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑎, 𝑏⟩ ∈ ( 𝑢) ↔ (⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢))
101 opelxp 5710 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋) ↔ (𝑎𝑋𝑏𝑋))
102101anbi1i 625 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢) ↔ ((𝑎𝑋𝑏𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢))
103 df-ov 7406 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 𝑏) = ( ‘⟨𝑎, 𝑏⟩)
104 oveq12 7412 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑧 = 𝑎𝑤 = 𝑏) → (𝑧(-g𝐺)𝑤) = (𝑎(-g𝐺)𝑏))
105104eceq1d 8737 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 = 𝑎𝑤 = 𝑏) → [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
106 ecexg 8702 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ~QG 𝑌) ∈ V → [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ V)
1078, 106ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ V
108105, 66, 107ovmpoa 7557 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝑋𝑏𝑋) → (𝑎 𝑏) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
109103, 108eqtr3id 2787 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎𝑋𝑏𝑋) → ( ‘⟨𝑎, 𝑏⟩) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
110109eleq1d 2819 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎𝑋𝑏𝑋) → (( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢 ↔ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢))
111110pm5.32i 576 . . . . . . . . . . . . . . . . . . . 20 (((𝑎𝑋𝑏𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢) ↔ ((𝑎𝑋𝑏𝑋) ∧ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢))
112100, 102, 1113bitri 297 . . . . . . . . . . . . . . . . . . 19 (⟨𝑎, 𝑏⟩ ∈ ( 𝑢) ↔ ((𝑎𝑋𝑏𝑋) ∧ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢))
113 eleq1 2822 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑡 ∈ (𝑐 × 𝑑) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑)))
114 opelxp 5710 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ↔ (𝑎𝑐𝑏𝑑))
115113, 114bitrdi 287 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑡 ∈ (𝑐 × 𝑑) ↔ (𝑎𝑐𝑏𝑑)))
116115anbi1d 631 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) ↔ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
1171162rexbidv 3220 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = ⟨𝑎, 𝑏⟩ → (∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) ↔ ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
118117rspccv 3608 . . . . . . . . . . . . . . . . . . 19 (∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) → (⟨𝑎, 𝑏⟩ ∈ ( 𝑢) → ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
119112, 118biimtrrid 242 . . . . . . . . . . . . . . . . . 18 (∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) → (((𝑎𝑋𝑏𝑋) ∧ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢) → ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
12095, 119syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (((𝑎𝑋𝑏𝑋) ∧ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢) → ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
12165, 120mpand 694 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ([(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢 → ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
122 simp-4l 782 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝐺 ∈ TopGrp)
12357adantr 482 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑌 ∈ (NrmSGrp‘𝐺))
124 simprll 778 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑐𝐽)
1251, 5, 13, 14, 7qustgpopn 23605 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑐𝐽) → (𝐹𝑐) ∈ 𝐾)
126122, 123, 124, 125syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑐) ∈ 𝐾)
127 simprlr 779 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑑𝐽)
1281, 5, 13, 14, 7qustgpopn 23605 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑑𝐽) → (𝐹𝑑) ∈ 𝐾)
129122, 123, 127, 128syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑑) ∈ 𝐾)
13058adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑎𝑋)
131 eceq1 8736 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑎 → [𝑥](𝐺 ~QG 𝑌) = [𝑎](𝐺 ~QG 𝑌))
132131, 7, 78fvmpt3i 6998 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎𝑋 → (𝐹𝑎) = [𝑎](𝐺 ~QG 𝑌))
133130, 132syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑎) = [𝑎](𝐺 ~QG 𝑌))
134122, 16syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝐽 ∈ (TopOn‘𝑋))
135 toponss 22410 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑐𝐽) → 𝑐𝑋)
136134, 124, 135syl2anc 585 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑐𝑋)
137 simprrl 780 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝑎𝑐𝑏𝑑))
138137simpld 496 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑎𝑐)
139 fnfvima 7229 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 Fn 𝑋𝑐𝑋𝑎𝑐) → (𝐹𝑎) ∈ (𝐹𝑐))
14079, 136, 138, 139mp3an2i 1467 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑎) ∈ (𝐹𝑐))
141133, 140eqeltrrd 2835 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → [𝑎](𝐺 ~QG 𝑌) ∈ (𝐹𝑐))
14259adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑏𝑋)
143 eceq1 8736 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑏 → [𝑥](𝐺 ~QG 𝑌) = [𝑏](𝐺 ~QG 𝑌))
144143, 7, 78fvmpt3i 6998 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏𝑋 → (𝐹𝑏) = [𝑏](𝐺 ~QG 𝑌))
145142, 144syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑏) = [𝑏](𝐺 ~QG 𝑌))
146 toponss 22410 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑑𝐽) → 𝑑𝑋)
147134, 127, 146syl2anc 585 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑑𝑋)
148137simprd 497 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑏𝑑)
149 fnfvima 7229 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 Fn 𝑋𝑑𝑋𝑏𝑑) → (𝐹𝑏) ∈ (𝐹𝑑))
15079, 147, 148, 149mp3an2i 1467 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑏) ∈ (𝐹𝑑))
151145, 150eqeltrrd 2835 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → [𝑏](𝐺 ~QG 𝑌) ∈ (𝐹𝑑))
152141, 151opelxpd 5712 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑)))
153136sselda 3980 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ 𝑝𝑐) → 𝑝𝑋)
154147sselda 3980 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ 𝑞𝑑) → 𝑞𝑋)
155153, 154anim12dan 620 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → (𝑝𝑋𝑞𝑋))
156 eceq1 8736 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑝 → [𝑥](𝐺 ~QG 𝑌) = [𝑝](𝐺 ~QG 𝑌))
157156, 7, 78fvmpt3i 6998 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝𝑋 → (𝐹𝑝) = [𝑝](𝐺 ~QG 𝑌))
158 eceq1 8736 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑞 → [𝑥](𝐺 ~QG 𝑌) = [𝑞](𝐺 ~QG 𝑌))
159158, 7, 78fvmpt3i 6998 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑞𝑋 → (𝐹𝑞) = [𝑞](𝐺 ~QG 𝑌))
160 opeq12 4873 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹𝑝) = [𝑝](𝐺 ~QG 𝑌) ∧ (𝐹𝑞) = [𝑞](𝐺 ~QG 𝑌)) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ = ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩)
161157, 159, 160syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑝𝑋𝑞𝑋) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ = ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩)
162155, 161syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ = ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩)
163123adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → 𝑌 ∈ (NrmSGrp‘𝐺))
1641, 5, 24quseccl 19059 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑝𝑋) → [𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻))
1651, 5, 24quseccl 19059 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑞𝑋) → [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻))
166164, 165anim12dan 620 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝑝𝑋𝑞𝑋)) → ([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)))
167163, 155, 166syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)))
168 opelxpi 5711 . . . . . . . . . . . . . . . . . . . . . . . . 25 (([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)) → ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)))
169167, 168syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)))
1701, 5, 60, 27qussub 19063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑝𝑋𝑞𝑋) → ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
1711703expb 1121 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝑝𝑋𝑞𝑋)) → ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
172163, 155, 171syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
173 oveq12 7412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 = 𝑝𝑤 = 𝑞) → (𝑧(-g𝐺)𝑤) = (𝑝(-g𝐺)𝑞))
174173eceq1d 8737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑧 = 𝑝𝑤 = 𝑞) → [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
175 ecexg 8702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐺 ~QG 𝑌) ∈ V → [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌) ∈ V)
1768, 175ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌) ∈ V
177174, 66, 176ovmpoa 7557 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑝𝑋𝑞𝑋) → (𝑝 𝑞) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
178155, 177syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → (𝑝 𝑞) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
179172, 178eqtr4d 2776 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = (𝑝 𝑞))
180 df-ov 7406 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = ((-g𝐻)‘⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩)
181 df-ov 7406 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 𝑞) = ( ‘⟨𝑝, 𝑞⟩)
182179, 180, 1813eqtr3g 2796 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ((-g𝐻)‘⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩) = ( ‘⟨𝑝, 𝑞⟩))
183 opelxpi 5711 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑝𝑐𝑞𝑑) → ⟨𝑝, 𝑞⟩ ∈ (𝑐 × 𝑑))
184 simprrr 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝑐 × 𝑑) ⊆ ( 𝑢))
185184sselda 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ ⟨𝑝, 𝑞⟩ ∈ (𝑐 × 𝑑)) → ⟨𝑝, 𝑞⟩ ∈ ( 𝑢))
186183, 185sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨𝑝, 𝑞⟩ ∈ ( 𝑢))
187 elpreima 7054 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( Fn (𝑋 × 𝑋) → (⟨𝑝, 𝑞⟩ ∈ ( 𝑢) ↔ (⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑝, 𝑞⟩) ∈ 𝑢)))
18898, 187ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟨𝑝, 𝑞⟩ ∈ ( 𝑢) ↔ (⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑝, 𝑞⟩) ∈ 𝑢))
189188simprbi 498 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑝, 𝑞⟩ ∈ ( 𝑢) → ( ‘⟨𝑝, 𝑞⟩) ∈ 𝑢)
190186, 189syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ( ‘⟨𝑝, 𝑞⟩) ∈ 𝑢)
191182, 190eqeltrd 2834 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ((-g𝐻)‘⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩) ∈ 𝑢)
19252, 53syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (-g𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)))
193192ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → (-g𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)))
194 elpreima 7054 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((-g𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)) → (⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢) ↔ (⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧ ((-g𝐻)‘⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩) ∈ 𝑢)))
195193, 194syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → (⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢) ↔ (⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧ ((-g𝐻)‘⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩) ∈ 𝑢)))
196169, 191, 195mpbir2and 712 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢))
197162, 196eqeltrd 2834 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢))
198197ralrimivva 3201 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ∀𝑝𝑐𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢))
199 opeq1 4871 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = (𝐹𝑝) → ⟨𝑧, 𝑤⟩ = ⟨(𝐹𝑝), 𝑤⟩)
200199eleq1d 2819 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = (𝐹𝑝) → (⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
201200ralbidv 3178 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (𝐹𝑝) → (∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
202201ralima 7234 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 Fn 𝑋𝑐𝑋) → (∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
20379, 202mpan 689 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐𝑋 → (∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
204 opeq2 4872 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = (𝐹𝑞) → ⟨(𝐹𝑝), 𝑤⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩)
205204eleq1d 2819 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = (𝐹𝑞) → (⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
206205ralima 7234 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 Fn 𝑋𝑑𝑋) → (∀𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
20779, 206mpan 689 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑𝑋 → (∀𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
208207ralbidv 3178 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑𝑋 → (∀𝑝𝑐𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
209203, 208sylan9bb 511 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑐𝑋𝑑𝑋) → (∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
210136, 147, 209syl2anc 585 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
211198, 210mpbird 257 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢))
212 dfss3 3968 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢) ↔ ∀𝑦 ∈ ((𝐹𝑐) × (𝐹𝑑))𝑦 ∈ ((-g𝐻) “ 𝑢))
213 eleq1 2822 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = ⟨𝑧, 𝑤⟩ → (𝑦 ∈ ((-g𝐻) “ 𝑢) ↔ ⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
214213ralxp 5838 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦 ∈ ((𝐹𝑐) × (𝐹𝑑))𝑦 ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢))
215212, 214bitri 275 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢) ↔ ∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢))
216211, 215sylibr 233 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢))
217 xpeq1 5688 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟 = (𝐹𝑐) → (𝑟 × 𝑠) = ((𝐹𝑐) × 𝑠))
218217eleq2d 2820 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = (𝐹𝑐) → (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × 𝑠)))
219217sseq1d 4011 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = (𝐹𝑐) → ((𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢) ↔ ((𝐹𝑐) × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
220218, 219anbi12d 632 . . . . . . . . . . . . . . . . . . . 20 (𝑟 = (𝐹𝑐) → ((⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × 𝑠) ∧ ((𝐹𝑐) × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
221 xpeq2 5695 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝐹𝑑) → ((𝐹𝑐) × 𝑠) = ((𝐹𝑐) × (𝐹𝑑)))
222221eleq2d 2820 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝐹𝑑) → (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × 𝑠) ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑))))
223221sseq1d 4011 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝐹𝑑) → (((𝐹𝑐) × 𝑠) ⊆ ((-g𝐻) “ 𝑢) ↔ ((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢)))
224222, 223anbi12d 632 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = (𝐹𝑑) → ((⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × 𝑠) ∧ ((𝐹𝑐) × 𝑠) ⊆ ((-g𝐻) “ 𝑢)) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑)) ∧ ((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢))))
225220, 224rspc2ev 3622 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑐) ∈ 𝐾 ∧ (𝐹𝑑) ∈ 𝐾 ∧ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑)) ∧ ((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢))) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
226126, 129, 152, 216, 225syl112anc 1375 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
227226expr 458 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑐𝐽𝑑𝐽)) → (((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
228227rexlimdvva 3212 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
229121, 228syld 47 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ([(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢 → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
23064, 229sylbid 239 . . . . . . . . . . . . . 14 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩) ∈ 𝑢 → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
231230adantld 492 . . . . . . . . . . . . 13 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ((⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧ ((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩) ∈ 𝑢) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
23255, 231sylbid 239 . . . . . . . . . . . 12 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
233 opeq12 4873 . . . . . . . . . . . . . 14 ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → ⟨𝑥, 𝑦⟩ = ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩)
234233eleq1d 2819 . . . . . . . . . . . . 13 ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢)))
235233eleq1d 2819 . . . . . . . . . . . . . 14 ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))} ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))}))
236 opex 5462 . . . . . . . . . . . . . . 15 ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ V
237 eleq1 2822 . . . . . . . . . . . . . . . . 17 (𝑤 = ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ → (𝑤 ∈ (𝑟 × 𝑠) ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠)))
238237anbi1d 631 . . . . . . . . . . . . . . . 16 (𝑤 = ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ → ((𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
2392382rexbidv 3220 . . . . . . . . . . . . . . 15 (𝑤 = ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ → (∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)) ↔ ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
240236, 239elab 3666 . . . . . . . . . . . . . 14 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))} ↔ ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
241235, 240bitrdi 287 . . . . . . . . . . . . 13 ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))} ↔ ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
242234, 241imbi12d 345 . . . . . . . . . . . 12 ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → ((⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) → ⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))}) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))))
243232, 242syl5ibrcom 246 . . . . . . . . . . 11 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) → ⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))})))
244243rexlimdvva 3212 . . . . . . . . . 10 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (∃𝑎𝑋𝑏𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) → ⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))})))
24550, 244sylbird 260 . . . . . . . . 9 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) → ⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))})))
246245com23 86 . . . . . . . 8 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) → (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)) → ⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))})))
24737, 246mpdd 43 . . . . . . 7 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) → ⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))}))
24836, 247relssdv 5785 . . . . . 6 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ((-g𝐻) “ 𝑢) ⊆ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))})
249 ssabral 4057 . . . . . 6 (((-g𝐻) “ 𝑢) ⊆ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))} ↔ ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
250248, 249sylib 217 . . . . 5 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
251 eltx 23053 . . . . . . 7 ((𝐾 ∈ (TopOn‘(Base‘𝐻)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → (((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
25223, 23, 251syl2anc 585 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
253252adantr 482 . . . . 5 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
254250, 253mpbird 257 . . . 4 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾))
255254ralrimiva 3147 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ∀𝑢𝐾 ((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾))
256 txtopon 23076 . . . . 5 ((𝐾 ∈ (TopOn‘(Base‘𝐻)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → (𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻))))
25723, 23, 256syl2anc 585 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻))))
258 iscn 22720 . . . 4 (((𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻))) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → ((-g𝐻) ∈ ((𝐾 ×t 𝐾) Cn 𝐾) ↔ ((-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) ∧ ∀𝑢𝐾 ((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾))))
259257, 23, 258syl2anc 585 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ((-g𝐻) ∈ ((𝐾 ×t 𝐾) Cn 𝐾) ↔ ((-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) ∧ ∀𝑢𝐾 ((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾))))
26029, 255, 259mpbir2and 712 . 2 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐻) ∈ ((𝐾 ×t 𝐾) Cn 𝐾))
26114, 27istgp2 23576 . 2 (𝐻 ∈ TopGrp ↔ (𝐻 ∈ Grp ∧ 𝐻 ∈ TopSp ∧ (-g𝐻) ∈ ((𝐾 ×t 𝐾) Cn 𝐾)))
2623, 26, 260, 261syl3anbrc 1344 1 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopGrp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  {cab 2710  wral 3062  wrex 3071  Vcvv 3475  wss 3946  cop 4632  cmpt 5229   × cxp 5672  ccnv 5673  dom cdm 5674  cima 5677  Rel wrel 5679   Fn wfn 6534  wf 6535  ontowfo 6537  cfv 6539  (class class class)co 7403  cmpo 7405  [cec 8696   / cqs 8697  Basecbs 17139  TopOpenctopn 17362   qTop cqtop 17444   /s cqus 17446  Grpcgrp 18814  -gcsg 18816  NrmSGrpcnsg 18994   ~QG cqg 18995  TopOnctopon 22393  TopSpctps 22415   Cn ccn 22709   ×t ctx 23045  TopGrpctgp 23556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5283  ax-sep 5297  ax-nul 5304  ax-pow 5361  ax-pr 5425  ax-un 7719  ax-cnex 11161  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-addrcl 11166  ax-mulcl 11167  ax-mulrcl 11168  ax-mulcom 11169  ax-addass 11170  ax-mulass 11171  ax-distr 11172  ax-i2m1 11173  ax-1ne0 11174  ax-1rid 11175  ax-rnegex 11176  ax-rrecex 11177  ax-cnre 11178  ax-pre-lttri 11179  ax-pre-lttrn 11180  ax-pre-ltadd 11181  ax-pre-mulgt0 11182
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3965  df-nul 4321  df-if 4527  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4907  df-iun 4997  df-br 5147  df-opab 5209  df-mpt 5230  df-tr 5264  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-pred 6296  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6491  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-riota 7359  df-ov 7406  df-oprab 7407  df-mpo 7408  df-om 7850  df-1st 7969  df-2nd 7970  df-tpos 8205  df-frecs 8260  df-wrecs 8291  df-recs 8365  df-rdg 8404  df-1o 8460  df-er 8698  df-ec 8700  df-qs 8704  df-map 8817  df-en 8935  df-dom 8936  df-sdom 8937  df-fin 8938  df-sup 9432  df-inf 9433  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249  df-sub 11441  df-neg 11442  df-nn 12208  df-2 12270  df-3 12271  df-4 12272  df-5 12273  df-6 12274  df-7 12275  df-8 12276  df-9 12277  df-n0 12468  df-z 12554  df-dec 12673  df-uz 12818  df-fz 13480  df-struct 17075  df-sets 17092  df-slot 17110  df-ndx 17122  df-base 17140  df-ress 17169  df-plusg 17205  df-mulr 17206  df-sca 17208  df-vsca 17209  df-ip 17210  df-tset 17211  df-ple 17212  df-ds 17214  df-rest 17363  df-topn 17364  df-0g 17382  df-topgen 17384  df-qtop 17448  df-imas 17449  df-qus 17450  df-plusf 18555  df-mgm 18556  df-sgrp 18605  df-mnd 18621  df-grp 18817  df-minusg 18818  df-sbg 18819  df-subg 18996  df-nsg 18997  df-eqg 18998  df-oppg 19202  df-top 22377  df-topon 22394  df-topsp 22416  df-bases 22430  df-cn 22712  df-cnp 22713  df-tx 23047  df-hmeo 23240  df-tmd 23557  df-tgp 23558
This theorem is referenced by:  qustgp  23607
  Copyright terms: Public domain W3C validator