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

Theorem qustgplem 24145
Description: Lemma for qustgp 24146. (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 19217 . . 3 (𝑌 ∈ (NrmSGrp‘𝐺) → 𝐻 ∈ Grp)
32adantl 481 . 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 7464 . . . . . . . 8 (𝐺 ~QG 𝑌) ∈ V
98a1i 11 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐺 ~QG 𝑌) ∈ V)
10 simpl 482 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐺 ∈ TopGrp)
114, 6, 7, 9, 10qusval 17589 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 = (𝐹s 𝐺))
124, 6, 7, 9, 10quslem 17590 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹:𝑋onto→(𝑋 / (𝐺 ~QG 𝑌)))
13 qustgpopn.j . . . . . 6 𝐽 = (TopOpen‘𝐺)
14 qustgpopn.k . . . . . 6 𝐾 = (TopOpen‘𝐻)
1511, 6, 12, 10, 13, 14imastopn 23744 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 = (𝐽 qTop 𝐹))
1613, 5tgptopon 24106 . . . . . . 7 (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋))
1716adantr 480 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐽 ∈ (TopOn‘𝑋))
18 qtoptopon 23728 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto→(𝑋 / (𝐺 ~QG 𝑌))) → (𝐽 qTop 𝐹) ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))))
1917, 12, 18syl2anc 584 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐽 qTop 𝐹) ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))))
2015, 19eqeltrd 2839 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))))
214, 6, 9, 10qusbas 17592 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑋 / (𝐺 ~QG 𝑌)) = (Base‘𝐻))
2221fveq2d 6911 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))) = (TopOn‘(Base‘𝐻)))
2320, 22eleqtrd 2841 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 ∈ (TopOn‘(Base‘𝐻)))
24 eqid 2735 . . . 4 (Base‘𝐻) = (Base‘𝐻)
2524, 14istps 22956 . . 3 (𝐻 ∈ TopSp ↔ 𝐾 ∈ (TopOn‘(Base‘𝐻)))
2623, 25sylibr 234 . 2 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopSp)
27 eqid 2735 . . . . 5 (-g𝐻) = (-g𝐻)
2824, 27grpsubf 19050 . . . 4 (𝐻 ∈ Grp → (-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻))
293, 28syl 17 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻))
30 cnvimass 6102 . . . . . . . . 9 ((-g𝐻) “ 𝑢) ⊆ dom (-g𝐻)
3129fdmd 6747 . . . . . . . . . 10 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → dom (-g𝐻) = ((Base‘𝐻) × (Base‘𝐻)))
3231adantr 480 . . . . . . . . 9 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → dom (-g𝐻) = ((Base‘𝐻) × (Base‘𝐻)))
3330, 32sseqtrid 4048 . . . . . . . 8 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ((-g𝐻) “ 𝑢) ⊆ ((Base‘𝐻) × (Base‘𝐻)))
34 relxp 5707 . . . . . . . 8 Rel ((Base‘𝐻) × (Base‘𝐻))
35 relss 5794 . . . . . . . 8 (((-g𝐻) “ 𝑢) ⊆ ((Base‘𝐻) × (Base‘𝐻)) → (Rel ((Base‘𝐻) × (Base‘𝐻)) → Rel ((-g𝐻) “ 𝑢)))
3633, 34, 35mpisyl 21 . . . . . . 7 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → Rel ((-g𝐻) “ 𝑢))
3733sseld 3994 . . . . . . . 8 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐻) × (Base‘𝐻))))
38 vex 3482 . . . . . . . . . . . . . 14 𝑥 ∈ V
3938elqs 8808 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ ∃𝑎𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌))
4021adantr 480 . . . . . . . . . . . . . 14 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (𝑋 / (𝐺 ~QG 𝑌)) = (Base‘𝐻))
4140eleq2d 2825 . . . . . . . . . . . . 13 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (𝑥 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ 𝑥 ∈ (Base‘𝐻)))
4239, 41bitr3id 285 . . . . . . . . . . . 12 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (∃𝑎𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ↔ 𝑥 ∈ (Base‘𝐻)))
43 vex 3482 . . . . . . . . . . . . . 14 𝑦 ∈ V
4443elqs 8808 . . . . . . . . . . . . 13 (𝑦 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ ∃𝑏𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌))
4540eleq2d 2825 . . . . . . . . . . . . 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 5725 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻)))
5047, 48, 493bitr4g 314 . . . . . . . . . 10 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (∃𝑎𝑋𝑏𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐻) × (Base‘𝐻))))
513ad2antrr 726 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝐻 ∈ Grp)
5251, 28syl 17 . . . . . . . . . . . . . 14 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻))
53 ffn 6737 . . . . . . . . . . . . . 14 ((-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) → (-g𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)))
54 elpreima 7078 . . . . . . . . . . . . . 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 7434 . . . . . . . . . . . . . . . . 17 ([𝑎](𝐺 ~QG 𝑌)(-g𝐻)[𝑏](𝐺 ~QG 𝑌)) = ((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩)
57 simpllr 776 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝑌 ∈ (NrmSGrp‘𝐺))
58 simprl 771 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝑎𝑋)
59 simprr 773 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝑏𝑋)
60 eqid 2735 . . . . . . . . . . . . . . . . . . 19 (-g𝐺) = (-g𝐺)
611, 5, 60, 27qussub 19222 . . . . . . . . . . . . . . . . . 18 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑎𝑋𝑏𝑋) → ([𝑎](𝐺 ~QG 𝑌)(-g𝐻)[𝑏](𝐺 ~QG 𝑌)) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
6257, 58, 59, 61syl3anc 1370 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ([𝑎](𝐺 ~QG 𝑌)(-g𝐻)[𝑏](𝐺 ~QG 𝑌)) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
6356, 62eqtr3id 2789 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
6463eleq1d 2824 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩) ∈ 𝑢 ↔ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢))
65 simpr 484 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (𝑎𝑋𝑏𝑋))
66 qustgplem.m . . . . . . . . . . . . . . . . . . . . . 22 = (𝑧𝑋, 𝑤𝑋 ↦ [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌))
67 tgpgrp 24102 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
6867adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐺 ∈ Grp)
695, 60grpsubf 19050 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐺 ∈ Grp → (-g𝐺):(𝑋 × 𝑋)⟶𝑋)
70 ffn 6737 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((-g𝐺):(𝑋 × 𝑋)⟶𝑋 → (-g𝐺) Fn (𝑋 × 𝑋))
7168, 69, 703syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐺) Fn (𝑋 × 𝑋))
72 fnov 7564 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((-g𝐺) Fn (𝑋 × 𝑋) ↔ (-g𝐺) = (𝑧𝑋, 𝑤𝑋 ↦ (𝑧(-g𝐺)𝑤)))
7371, 72sylib 218 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐺) = (𝑧𝑋, 𝑤𝑋 ↦ (𝑧(-g𝐺)𝑤)))
7413, 60tgpsubcn 24114 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐺 ∈ TopGrp → (-g𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
7574adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
7673, 75eqeltrrd 2840 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑧𝑋, 𝑤𝑋 ↦ (𝑧(-g𝐺)𝑤)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
77 ecexg 8748 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐺 ~QG 𝑌) ∈ V → [𝑥](𝐺 ~QG 𝑌) ∈ V)
788, 77ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 [𝑥](𝐺 ~QG 𝑌) ∈ V
7978, 7fnmpti 6712 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝐹 Fn 𝑋
80 qtopid 23729 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 Fn 𝑋) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)))
8117, 79, 80sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)))
8215oveq2d 7447 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐽 Cn 𝐾) = (𝐽 Cn (𝐽 qTop 𝐹)))
8381, 82eleqtrrd 2842 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹 ∈ (𝐽 Cn 𝐾))
847, 83eqeltrrid 2844 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑥𝑋 ↦ [𝑥](𝐺 ~QG 𝑌)) ∈ (𝐽 Cn 𝐾))
85 eceq1 8783 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑧(-g𝐺)𝑤) → [𝑥](𝐺 ~QG 𝑌) = [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌))
8617, 17, 76, 17, 84, 85cnmpt21 23695 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑧𝑋, 𝑤𝑋 ↦ [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌)) ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
8766, 86eqeltrid 2843 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
8887ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
89 simplr 769 . . . . . . . . . . . . . . . . . . . 20 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝑢𝐾)
90 cnima 23289 . . . . . . . . . . . . . . . . . . . 20 (( ∈ ((𝐽 ×t 𝐽) Cn 𝐾) ∧ 𝑢𝐾) → ( 𝑢) ∈ (𝐽 ×t 𝐽))
9188, 89, 90syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ( 𝑢) ∈ (𝐽 ×t 𝐽))
9217ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
93 eltx 23592 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘𝑋)) → (( 𝑢) ∈ (𝐽 ×t 𝐽) ↔ ∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
9492, 92, 93syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (( 𝑢) ∈ (𝐽 ×t 𝐽) ↔ ∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
9591, 94mpbid 232 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))
96 ecexg 8748 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ~QG 𝑌) ∈ V → [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌) ∈ V)
978, 96ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌) ∈ V
9866, 97fnmpoi 8094 . . . . . . . . . . . . . . . . . . . . 21 Fn (𝑋 × 𝑋)
99 elpreima 7078 . . . . . . . . . . . . . . . . . . . . 21 ( Fn (𝑋 × 𝑋) → (⟨𝑎, 𝑏⟩ ∈ ( 𝑢) ↔ (⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢)))
10098, 99ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑎, 𝑏⟩ ∈ ( 𝑢) ↔ (⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢))
101 opelxp 5725 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋) ↔ (𝑎𝑋𝑏𝑋))
102101anbi1i 624 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢) ↔ ((𝑎𝑋𝑏𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢))
103 df-ov 7434 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 𝑏) = ( ‘⟨𝑎, 𝑏⟩)
104 oveq12 7440 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑧 = 𝑎𝑤 = 𝑏) → (𝑧(-g𝐺)𝑤) = (𝑎(-g𝐺)𝑏))
105104eceq1d 8784 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 = 𝑎𝑤 = 𝑏) → [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
106 ecexg 8748 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ~QG 𝑌) ∈ V → [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ V)
1078, 106ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ V
108105, 66, 107ovmpoa 7588 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝑋𝑏𝑋) → (𝑎 𝑏) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
109103, 108eqtr3id 2789 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎𝑋𝑏𝑋) → ( ‘⟨𝑎, 𝑏⟩) = [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌))
110109eleq1d 2824 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎𝑋𝑏𝑋) → (( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢 ↔ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢))
111110pm5.32i 574 . . . . . . . . . . . . . . . . . . . 20 (((𝑎𝑋𝑏𝑋) ∧ ( ‘⟨𝑎, 𝑏⟩) ∈ 𝑢) ↔ ((𝑎𝑋𝑏𝑋) ∧ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢))
112100, 102, 1113bitri 297 . . . . . . . . . . . . . . . . . . 19 (⟨𝑎, 𝑏⟩ ∈ ( 𝑢) ↔ ((𝑎𝑋𝑏𝑋) ∧ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢))
113 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑡 ∈ (𝑐 × 𝑑) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑)))
114 opelxp 5725 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ↔ (𝑎𝑐𝑏𝑑))
115113, 114bitrdi 287 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑡 ∈ (𝑐 × 𝑑) ↔ (𝑎𝑐𝑏𝑑)))
116115anbi1d 631 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) ↔ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
1171162rexbidv 3220 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = ⟨𝑎, 𝑏⟩ → (∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) ↔ ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
118117rspccv 3619 . . . . . . . . . . . . . . . . . . 19 (∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) → (⟨𝑎, 𝑏⟩ ∈ ( 𝑢) → ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
119112, 118biimtrrid 243 . . . . . . . . . . . . . . . . . 18 (∀𝑡 ∈ ( 𝑢)∃𝑐𝐽𝑑𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) → (((𝑎𝑋𝑏𝑋) ∧ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢) → ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
12095, 119syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (((𝑎𝑋𝑏𝑋) ∧ [(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢) → ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
12165, 120mpand 695 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ([(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢 → ∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢))))
122 simp-4l 783 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝐺 ∈ TopGrp)
12357adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑌 ∈ (NrmSGrp‘𝐺))
124 simprll 779 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑐𝐽)
1251, 5, 13, 14, 7qustgpopn 24144 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑐𝐽) → (𝐹𝑐) ∈ 𝐾)
126122, 123, 124, 125syl3anc 1370 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑐) ∈ 𝐾)
127 simprlr 780 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑑𝐽)
1281, 5, 13, 14, 7qustgpopn 24144 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑑𝐽) → (𝐹𝑑) ∈ 𝐾)
129122, 123, 127, 128syl3anc 1370 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑑) ∈ 𝐾)
13058adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑎𝑋)
131 eceq1 8783 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑎 → [𝑥](𝐺 ~QG 𝑌) = [𝑎](𝐺 ~QG 𝑌))
132131, 7, 78fvmpt3i 7021 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎𝑋 → (𝐹𝑎) = [𝑎](𝐺 ~QG 𝑌))
133130, 132syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑎) = [𝑎](𝐺 ~QG 𝑌))
134122, 16syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝐽 ∈ (TopOn‘𝑋))
135 toponss 22949 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑐𝐽) → 𝑐𝑋)
136134, 124, 135syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑐𝑋)
137 simprrl 781 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝑎𝑐𝑏𝑑))
138137simpld 494 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑎𝑐)
139 fnfvima 7253 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 Fn 𝑋𝑐𝑋𝑎𝑐) → (𝐹𝑎) ∈ (𝐹𝑐))
14079, 136, 138, 139mp3an2i 1465 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑎) ∈ (𝐹𝑐))
141133, 140eqeltrrd 2840 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → [𝑎](𝐺 ~QG 𝑌) ∈ (𝐹𝑐))
14259adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑏𝑋)
143 eceq1 8783 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑏 → [𝑥](𝐺 ~QG 𝑌) = [𝑏](𝐺 ~QG 𝑌))
144143, 7, 78fvmpt3i 7021 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏𝑋 → (𝐹𝑏) = [𝑏](𝐺 ~QG 𝑌))
145142, 144syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑏) = [𝑏](𝐺 ~QG 𝑌))
146 toponss 22949 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑑𝐽) → 𝑑𝑋)
147134, 127, 146syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑑𝑋)
148137simprd 495 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → 𝑏𝑑)
149 fnfvima 7253 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 Fn 𝑋𝑑𝑋𝑏𝑑) → (𝐹𝑏) ∈ (𝐹𝑑))
15079, 147, 148, 149mp3an2i 1465 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝐹𝑏) ∈ (𝐹𝑑))
151145, 150eqeltrrd 2840 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → [𝑏](𝐺 ~QG 𝑌) ∈ (𝐹𝑑))
152141, 151opelxpd 5728 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑)))
153136sselda 3995 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ 𝑝𝑐) → 𝑝𝑋)
154147sselda 3995 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ 𝑞𝑑) → 𝑞𝑋)
155153, 154anim12dan 619 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → (𝑝𝑋𝑞𝑋))
156 eceq1 8783 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑝 → [𝑥](𝐺 ~QG 𝑌) = [𝑝](𝐺 ~QG 𝑌))
157156, 7, 78fvmpt3i 7021 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝𝑋 → (𝐹𝑝) = [𝑝](𝐺 ~QG 𝑌))
158 eceq1 8783 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑞 → [𝑥](𝐺 ~QG 𝑌) = [𝑞](𝐺 ~QG 𝑌))
159158, 7, 78fvmpt3i 7021 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑞𝑋 → (𝐹𝑞) = [𝑞](𝐺 ~QG 𝑌))
160 opeq12 4880 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹𝑝) = [𝑝](𝐺 ~QG 𝑌) ∧ (𝐹𝑞) = [𝑞](𝐺 ~QG 𝑌)) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ = ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩)
161157, 159, 160syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑝𝑋𝑞𝑋) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ = ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩)
162155, 161syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ = ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩)
163123adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → 𝑌 ∈ (NrmSGrp‘𝐺))
1641, 5, 24quseccl 19218 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑝𝑋) → [𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻))
1651, 5, 24quseccl 19218 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑞𝑋) → [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻))
166164, 165anim12dan 619 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝑝𝑋𝑞𝑋)) → ([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)))
167163, 155, 166syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)))
168 opelxpi 5726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)) → ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)))
169167, 168syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)))
1701, 5, 60, 27qussub 19222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑝𝑋𝑞𝑋) → ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
1711703expb 1119 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝑝𝑋𝑞𝑋)) → ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
172163, 155, 171syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
173 oveq12 7440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 = 𝑝𝑤 = 𝑞) → (𝑧(-g𝐺)𝑤) = (𝑝(-g𝐺)𝑞))
174173eceq1d 8784 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑧 = 𝑝𝑤 = 𝑞) → [(𝑧(-g𝐺)𝑤)](𝐺 ~QG 𝑌) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
175 ecexg 8748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐺 ~QG 𝑌) ∈ V → [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌) ∈ V)
1768, 175ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌) ∈ V
177174, 66, 176ovmpoa 7588 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑝𝑋𝑞𝑋) → (𝑝 𝑞) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
178155, 177syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → (𝑝 𝑞) = [(𝑝(-g𝐺)𝑞)](𝐺 ~QG 𝑌))
179172, 178eqtr4d 2778 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = (𝑝 𝑞))
180 df-ov 7434 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑝](𝐺 ~QG 𝑌)(-g𝐻)[𝑞](𝐺 ~QG 𝑌)) = ((-g𝐻)‘⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩)
181 df-ov 7434 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 𝑞) = ( ‘⟨𝑝, 𝑞⟩)
182179, 180, 1813eqtr3g 2798 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ((-g𝐻)‘⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩) = ( ‘⟨𝑝, 𝑞⟩))
183 opelxpi 5726 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑝𝑐𝑞𝑑) → ⟨𝑝, 𝑞⟩ ∈ (𝑐 × 𝑑))
184 simprrr 782 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (𝑐 × 𝑑) ⊆ ( 𝑢))
185184sselda 3995 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ ⟨𝑝, 𝑞⟩ ∈ (𝑐 × 𝑑)) → ⟨𝑝, 𝑞⟩ ∈ ( 𝑢))
186183, 185sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨𝑝, 𝑞⟩ ∈ ( 𝑢))
187 elpreima 7078 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( Fn (𝑋 × 𝑋) → (⟨𝑝, 𝑞⟩ ∈ ( 𝑢) ↔ (⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑝, 𝑞⟩) ∈ 𝑢)))
18898, 187ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟨𝑝, 𝑞⟩ ∈ ( 𝑢) ↔ (⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋) ∧ ( ‘⟨𝑝, 𝑞⟩) ∈ 𝑢))
189188simprbi 496 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑝, 𝑞⟩ ∈ ( 𝑢) → ( ‘⟨𝑝, 𝑞⟩) ∈ 𝑢)
190186, 189syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ( ‘⟨𝑝, 𝑞⟩) ∈ 𝑢)
191182, 190eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ((-g𝐻)‘⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩) ∈ 𝑢)
19252, 53syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (-g𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)))
193192ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → (-g𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)))
194 elpreima 7078 . . . . . . . . . . . . . . . . . . . . . . . . 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 713 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢))
197162, 196eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) ∧ (𝑝𝑐𝑞𝑑)) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢))
198197ralrimivva 3200 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ∀𝑝𝑐𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢))
199 opeq1 4878 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = (𝐹𝑝) → ⟨𝑧, 𝑤⟩ = ⟨(𝐹𝑝), 𝑤⟩)
200199eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = (𝐹𝑝) → (⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
201200ralbidv 3176 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (𝐹𝑝) → (∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
202201ralima 7257 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 Fn 𝑋𝑐𝑋) → (∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
20379, 202mpan 690 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐𝑋 → (∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
204 opeq2 4879 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = (𝐹𝑞) → ⟨(𝐹𝑝), 𝑤⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩)
205204eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = (𝐹𝑞) → (⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
206205ralima 7257 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 Fn 𝑋𝑑𝑋) → (∀𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
20779, 206mpan 690 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑𝑋 → (∀𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
208207ralbidv 3176 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑𝑋 → (∀𝑝𝑐𝑤 ∈ (𝐹𝑑)⟨(𝐹𝑝), 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
209203, 208sylan9bb 509 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑐𝑋𝑑𝑋) → (∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
210136, 147, 209syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → (∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑝𝑐𝑞𝑑 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ ((-g𝐻) “ 𝑢)))
211198, 210mpbird 257 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢))
212 dfss3 3984 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢) ↔ ∀𝑦 ∈ ((𝐹𝑐) × (𝐹𝑑))𝑦 ∈ ((-g𝐻) “ 𝑢))
213 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = ⟨𝑧, 𝑤⟩ → (𝑦 ∈ ((-g𝐻) “ 𝑢) ↔ ⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢)))
214213ralxp 5855 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦 ∈ ((𝐹𝑐) × (𝐹𝑑))𝑦 ∈ ((-g𝐻) “ 𝑢) ↔ ∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢))
215212, 214bitri 275 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢) ↔ ∀𝑧 ∈ (𝐹𝑐)∀𝑤 ∈ (𝐹𝑑)⟨𝑧, 𝑤⟩ ∈ ((-g𝐻) “ 𝑢))
216211, 215sylibr 234 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢))
217 xpeq1 5703 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟 = (𝐹𝑐) → (𝑟 × 𝑠) = ((𝐹𝑐) × 𝑠))
218217eleq2d 2825 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = (𝐹𝑐) → (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × 𝑠)))
219217sseq1d 4027 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = (𝐹𝑐) → ((𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢) ↔ ((𝐹𝑐) × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
220218, 219anbi12d 632 . . . . . . . . . . . . . . . . . . . 20 (𝑟 = (𝐹𝑐) → ((⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × 𝑠) ∧ ((𝐹𝑐) × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
221 xpeq2 5710 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝐹𝑑) → ((𝐹𝑐) × 𝑠) = ((𝐹𝑐) × (𝐹𝑑)))
222221eleq2d 2825 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝐹𝑑) → (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × 𝑠) ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑))))
223221sseq1d 4027 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝐹𝑑) → (((𝐹𝑐) × 𝑠) ⊆ ((-g𝐻) “ 𝑢) ↔ ((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢)))
224222, 223anbi12d 632 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = (𝐹𝑑) → ((⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × 𝑠) ∧ ((𝐹𝑐) × 𝑠) ⊆ ((-g𝐻) “ 𝑢)) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑)) ∧ ((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢))))
225220, 224rspc2ev 3635 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑐) ∈ 𝐾 ∧ (𝐹𝑑) ∈ 𝐾 ∧ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((𝐹𝑐) × (𝐹𝑑)) ∧ ((𝐹𝑐) × (𝐹𝑑)) ⊆ ((-g𝐻) “ 𝑢))) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
226126, 129, 152, 216, 225syl112anc 1373 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ ((𝑐𝐽𝑑𝐽) ∧ ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)))) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
227226expr 456 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) ∧ (𝑐𝐽𝑑𝐽)) → (((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
228227rexlimdvva 3211 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (∃𝑐𝐽𝑑𝐽 ((𝑎𝑐𝑏𝑑) ∧ (𝑐 × 𝑑) ⊆ ( 𝑢)) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
229121, 228syld 47 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ([(𝑎(-g𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢 → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
23064, 229sylbid 240 . . . . . . . . . . . . . 14 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩) ∈ 𝑢 → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
231230adantld 490 . . . . . . . . . . . . 13 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ((⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧ ((-g𝐻)‘⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩) ∈ 𝑢) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
23255, 231sylbid 240 . . . . . . . . . . . 12 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
233 opeq12 4880 . . . . . . . . . . . . . 14 ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → ⟨𝑥, 𝑦⟩ = ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩)
234233eleq1d 2824 . . . . . . . . . . . . 13 ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢)))
235233eleq1d 2824 . . . . . . . . . . . . . 14 ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))} ↔ ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))}))
236 opex 5475 . . . . . . . . . . . . . . 15 ⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ V
237 eleq1 2827 . . . . . . . . . . . . . . . . 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 3681 . . . . . . . . . . . . . 14 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))} ↔ ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
241235, 240bitrdi 287 . . . . . . . . . . . . 13 ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))} ↔ ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
242234, 241imbi12d 344 . . . . . . . . . . . 12 ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → ((⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) → ⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))}) ↔ (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ ((-g𝐻) “ 𝑢) → ∃𝑟𝐾𝑠𝐾 (⟨[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))))
243232, 242syl5ibrcom 247 . . . . . . . . . . 11 ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) ∧ (𝑎𝑋𝑏𝑋)) → ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐻) “ 𝑢) → ⟨𝑥, 𝑦⟩ ∈ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))})))
244243rexlimdvva 3211 . . . . . . . . . 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 5801 . . . . . 6 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ((-g𝐻) “ 𝑢) ⊆ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))})
249 ssabral 4075 . . . . . 6 (((-g𝐻) “ 𝑢) ⊆ {𝑤 ∣ ∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))} ↔ ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
250248, 249sylib 218 . . . . 5 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢)))
251 eltx 23592 . . . . . . 7 ((𝐾 ∈ (TopOn‘(Base‘𝐻)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → (((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
25223, 23, 251syl2anc 584 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
253252adantr 480 . . . . 5 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → (((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ ((-g𝐻) “ 𝑢)∃𝑟𝐾𝑠𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ ((-g𝐻) “ 𝑢))))
254250, 253mpbird 257 . . . 4 (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢𝐾) → ((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾))
255254ralrimiva 3144 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ∀𝑢𝐾 ((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾))
256 txtopon 23615 . . . . 5 ((𝐾 ∈ (TopOn‘(Base‘𝐻)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → (𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻))))
25723, 23, 256syl2anc 584 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻))))
258 iscn 23259 . . . 4 (((𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻))) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → ((-g𝐻) ∈ ((𝐾 ×t 𝐾) Cn 𝐾) ↔ ((-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) ∧ ∀𝑢𝐾 ((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾))))
259257, 23, 258syl2anc 584 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ((-g𝐻) ∈ ((𝐾 ×t 𝐾) Cn 𝐾) ↔ ((-g𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) ∧ ∀𝑢𝐾 ((-g𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾))))
26029, 255, 259mpbir2and 713 . 2 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (-g𝐻) ∈ ((𝐾 ×t 𝐾) Cn 𝐾))
26114, 27istgp2 24115 . 2 (𝐻 ∈ TopGrp ↔ (𝐻 ∈ Grp ∧ 𝐻 ∈ TopSp ∧ (-g𝐻) ∈ ((𝐾 ×t 𝐾) Cn 𝐾)))
2623, 26, 260, 261syl3anbrc 1342 1 ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopGrp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106  {cab 2712  wral 3059  wrex 3068  Vcvv 3478  wss 3963  cop 4637  cmpt 5231   × cxp 5687  ccnv 5688  dom cdm 5689  cima 5692  Rel wrel 5694   Fn wfn 6558  wf 6559  ontowfo 6561  cfv 6563  (class class class)co 7431  cmpo 7433  [cec 8742   / cqs 8743  Basecbs 17245  TopOpenctopn 17468   qTop cqtop 17550   /s cqus 17552  Grpcgrp 18964  -gcsg 18966  NrmSGrpcnsg 19152   ~QG cqg 19153  TopOnctopon 22932  TopSpctps 22954   Cn ccn 23248   ×t ctx 23584  TopGrpctgp 24095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-tpos 8250  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-er 8744  df-ec 8746  df-qs 8750  df-map 8867  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-sup 9480  df-inf 9481  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-nn 12265  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12525  df-z 12612  df-dec 12732  df-uz 12877  df-fz 13545  df-struct 17181  df-sets 17198  df-slot 17216  df-ndx 17228  df-base 17246  df-ress 17275  df-plusg 17311  df-mulr 17312  df-sca 17314  df-vsca 17315  df-ip 17316  df-tset 17317  df-ple 17318  df-ds 17320  df-rest 17469  df-topn 17470  df-0g 17488  df-topgen 17490  df-qtop 17554  df-imas 17555  df-qus 17556  df-plusf 18665  df-mgm 18666  df-sgrp 18745  df-mnd 18761  df-grp 18967  df-minusg 18968  df-sbg 18969  df-subg 19154  df-nsg 19155  df-eqg 19156  df-oppg 19377  df-top 22916  df-topon 22933  df-topsp 22955  df-bases 22969  df-cn 23251  df-cnp 23252  df-tx 23586  df-hmeo 23779  df-tmd 24096  df-tgp 24097
This theorem is referenced by:  qustgp  24146
  Copyright terms: Public domain W3C validator