| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | qustgp.h | . . . 4
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌)) | 
| 2 | 1 | qusgrp 19205 | . . 3
⊢ (𝑌 ∈ (NrmSGrp‘𝐺) → 𝐻 ∈ Grp) | 
| 3 | 2 | adantl 481 | . 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ Grp) | 
| 4 | 1 | a1i 11 | . . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌))) | 
| 5 |  | qustgpopn.x | . . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) | 
| 6 | 5 | a1i 11 | . . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝑋 = (Base‘𝐺)) | 
| 7 |  | qustgpopn.f | . . . . . . 7
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ [𝑥](𝐺 ~QG 𝑌)) | 
| 8 |  | ovex 7465 | . . . . . . . 8
⊢ (𝐺 ~QG 𝑌) ∈ V | 
| 9 | 8 | a1i 11 | . . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐺 ~QG 𝑌) ∈ V) | 
| 10 |  | simpl 482 | . . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐺 ∈ TopGrp) | 
| 11 | 4, 6, 7, 9, 10 | qusval 17588 | . . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 = (𝐹 “s 𝐺)) | 
| 12 | 4, 6, 7, 9, 10 | quslem 17589 | . . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹:𝑋–onto→(𝑋 / (𝐺 ~QG 𝑌))) | 
| 13 |  | qustgpopn.j | . . . . . 6
⊢ 𝐽 = (TopOpen‘𝐺) | 
| 14 |  | qustgpopn.k | . . . . . 6
⊢ 𝐾 = (TopOpen‘𝐻) | 
| 15 | 11, 6, 12, 10, 13, 14 | imastopn 23729 | . . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 = (𝐽 qTop 𝐹)) | 
| 16 | 13, 5 | tgptopon 24091 | . . . . . . 7
⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋)) | 
| 17 | 16 | adantr 480 | . . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐽 ∈ (TopOn‘𝑋)) | 
| 18 |  | qtoptopon 23713 | . . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→(𝑋 / (𝐺 ~QG 𝑌))) → (𝐽 qTop 𝐹) ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌)))) | 
| 19 | 17, 12, 18 | syl2anc 584 | . . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐽 qTop 𝐹) ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌)))) | 
| 20 | 15, 19 | eqeltrd 2840 | . . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌)))) | 
| 21 | 4, 6, 9, 10 | qusbas 17591 | . . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑋 / (𝐺 ~QG 𝑌)) = (Base‘𝐻)) | 
| 22 | 21 | fveq2d 6909 | . . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))) = (TopOn‘(Base‘𝐻))) | 
| 23 | 20, 22 | eleqtrd 2842 | . . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 ∈ (TopOn‘(Base‘𝐻))) | 
| 24 |  | eqid 2736 | . . . 4
⊢
(Base‘𝐻) =
(Base‘𝐻) | 
| 25 | 24, 14 | istps 22941 | . . 3
⊢ (𝐻 ∈ TopSp ↔ 𝐾 ∈
(TopOn‘(Base‘𝐻))) | 
| 26 | 23, 25 | sylibr 234 | . 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopSp) | 
| 27 |  | eqid 2736 | . . . . 5
⊢
(-g‘𝐻) = (-g‘𝐻) | 
| 28 | 24, 27 | grpsubf 19038 | . . . 4
⊢ (𝐻 ∈ Grp →
(-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻)) | 
| 29 | 3, 28 | syl 17 | . . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
(-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻)) | 
| 30 |  | cnvimass 6099 | . . . . . . . . 9
⊢ (◡(-g‘𝐻) “ 𝑢) ⊆ dom (-g‘𝐻) | 
| 31 | 29 | fdmd 6745 | . . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → dom
(-g‘𝐻) =
((Base‘𝐻) ×
(Base‘𝐻))) | 
| 32 | 31 | adantr 480 | . . . . . . . . 9
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → dom (-g‘𝐻) = ((Base‘𝐻) × (Base‘𝐻))) | 
| 33 | 30, 32 | sseqtrid 4025 | . . . . . . . 8
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (◡(-g‘𝐻) “ 𝑢) ⊆ ((Base‘𝐻) × (Base‘𝐻))) | 
| 34 |  | relxp 5702 | . . . . . . . 8
⊢ Rel
((Base‘𝐻) ×
(Base‘𝐻)) | 
| 35 |  | relss 5790 | . . . . . . . 8
⊢ ((◡(-g‘𝐻) “ 𝑢) ⊆ ((Base‘𝐻) × (Base‘𝐻)) → (Rel ((Base‘𝐻) × (Base‘𝐻)) → Rel (◡(-g‘𝐻) “ 𝑢))) | 
| 36 | 33, 34, 35 | mpisyl 21 | . . . . . . 7
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → Rel (◡(-g‘𝐻) “ 𝑢)) | 
| 37 | 33 | sseld 3981 | . . . . . . . 8
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → 〈𝑥, 𝑦〉 ∈ ((Base‘𝐻) × (Base‘𝐻)))) | 
| 38 |  | vex 3483 | . . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V | 
| 39 | 38 | elqs 8810 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ ∃𝑎 ∈ 𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌)) | 
| 40 | 21 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (𝑋 / (𝐺 ~QG 𝑌)) = (Base‘𝐻)) | 
| 41 | 40 | eleq2d 2826 | . . . . . . . . . . . . 13
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (𝑥 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ 𝑥 ∈ (Base‘𝐻))) | 
| 42 | 39, 41 | bitr3id 285 | . . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (∃𝑎 ∈ 𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ↔ 𝑥 ∈ (Base‘𝐻))) | 
| 43 |  | vex 3483 | . . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V | 
| 44 | 43 | elqs 8810 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ ∃𝑏 ∈ 𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌)) | 
| 45 | 40 | eleq2d 2826 | . . . . . . . . . . . . 13
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (𝑦 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ 𝑦 ∈ (Base‘𝐻))) | 
| 46 | 44, 45 | bitr3id 285 | . . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (∃𝑏 ∈ 𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌) ↔ 𝑦 ∈ (Base‘𝐻))) | 
| 47 | 42, 46 | anbi12d 632 | . . . . . . . . . . 11
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → ((∃𝑎 ∈ 𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ ∃𝑏 ∈ 𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻)))) | 
| 48 |  | reeanv 3228 | . . . . . . . . . . 11
⊢
(∃𝑎 ∈
𝑋 ∃𝑏 ∈ 𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ (∃𝑎 ∈ 𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ ∃𝑏 ∈ 𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌))) | 
| 49 |  | opelxp 5720 | . . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) | 
| 50 | 47, 48, 49 | 3bitr4g 314 | . . . . . . . . . 10
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ 〈𝑥, 𝑦〉 ∈ ((Base‘𝐻) × (Base‘𝐻)))) | 
| 51 | 3 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝐻 ∈ Grp) | 
| 52 | 51, 28 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻)) | 
| 53 |  | ffn 6735 | . . . . . . . . . . . . . 14
⊢
((-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) → (-g‘𝐻) Fn ((Base‘𝐻) × (Base‘𝐻))) | 
| 54 |  | elpreima 7077 | . . . . . . . . . . . . . 14
⊢
((-g‘𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)) → (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧
((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) ∈ 𝑢))) | 
| 55 | 52, 53, 54 | 3syl 18 | . . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧
((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) ∈ 𝑢))) | 
| 56 |  | df-ov 7435 | . . . . . . . . . . . . . . . . 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 2736 | . . . . . . . . . . . . . . . . . . 19
⊢
(-g‘𝐺) = (-g‘𝐺) | 
| 61 | 1, 5, 60, 27 | qussub 19210 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ([𝑎](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑏](𝐺 ~QG 𝑌)) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) | 
| 62 | 57, 58, 59, 61 | syl3anc 1372 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ([𝑎](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑏](𝐺 ~QG 𝑌)) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) | 
| 63 | 56, 62 | eqtr3id 2790 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) | 
| 64 | 63 | eleq1d 2825 | . . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) ∈ 𝑢 ↔ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢)) | 
| 65 |  | simpr 484 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) | 
| 66 |  | qustgplem.m | . . . . . . . . . . . . . . . . . . . . . 22
⊢  − =
(𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌)) | 
| 67 |  | tgpgrp 24087 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) | 
| 68 | 67 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐺 ∈ Grp) | 
| 69 | 5, 60 | grpsubf 19038 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐺 ∈ Grp →
(-g‘𝐺):(𝑋 × 𝑋)⟶𝑋) | 
| 70 |  | ffn 6735 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((-g‘𝐺):(𝑋 × 𝑋)⟶𝑋 → (-g‘𝐺) Fn (𝑋 × 𝑋)) | 
| 71 | 68, 69, 70 | 3syl 18 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
(-g‘𝐺) Fn
(𝑋 × 𝑋)) | 
| 72 |  | fnov 7565 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((-g‘𝐺) Fn (𝑋 × 𝑋) ↔ (-g‘𝐺) = (𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ (𝑧(-g‘𝐺)𝑤))) | 
| 73 | 71, 72 | sylib 218 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
(-g‘𝐺) =
(𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ (𝑧(-g‘𝐺)𝑤))) | 
| 74 | 13, 60 | tgpsubcn 24099 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐺 ∈ TopGrp →
(-g‘𝐺)
∈ ((𝐽
×t 𝐽) Cn
𝐽)) | 
| 75 | 74 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
(-g‘𝐺)
∈ ((𝐽
×t 𝐽) Cn
𝐽)) | 
| 76 | 73, 75 | eqeltrrd 2841 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ (𝑧(-g‘𝐺)𝑤)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) | 
| 77 |  | ecexg 8750 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐺 ~QG 𝑌) ∈ V → [𝑥](𝐺 ~QG 𝑌) ∈ V) | 
| 78 | 8, 77 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ [𝑥](𝐺 ~QG 𝑌) ∈ V | 
| 79 | 78, 7 | fnmpti 6710 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝐹 Fn 𝑋 | 
| 80 |  | qtopid 23714 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 Fn 𝑋) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))) | 
| 81 | 17, 79, 80 | sylancl 586 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))) | 
| 82 | 15 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐽 Cn 𝐾) = (𝐽 Cn (𝐽 qTop 𝐹))) | 
| 83 | 81, 82 | eleqtrrd 2843 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹 ∈ (𝐽 Cn 𝐾)) | 
| 84 | 7, 83 | eqeltrrid 2845 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑥 ∈ 𝑋 ↦ [𝑥](𝐺 ~QG 𝑌)) ∈ (𝐽 Cn 𝐾)) | 
| 85 |  | eceq1 8785 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = (𝑧(-g‘𝐺)𝑤) → [𝑥](𝐺 ~QG 𝑌) = [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌)) | 
| 86 | 17, 17, 76, 17, 84, 85 | cnmpt21 23680 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌)) ∈ ((𝐽 ×t 𝐽) Cn 𝐾)) | 
| 87 | 66, 86 | eqeltrid 2844 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → − ∈ ((𝐽 ×t 𝐽) Cn 𝐾)) | 
| 88 | 87 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → − ∈ ((𝐽 ×t 𝐽) Cn 𝐾)) | 
| 89 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑢 ∈ 𝐾) | 
| 90 |  | cnima 23274 | . . . . . . . . . . . . . . . . . . . 20
⊢ (( − ∈
((𝐽 ×t
𝐽) Cn 𝐾) ∧ 𝑢 ∈ 𝐾) → (◡ − “ 𝑢) ∈ (𝐽 ×t 𝐽)) | 
| 91 | 88, 89, 90 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (◡ − “ 𝑢) ∈ (𝐽 ×t 𝐽)) | 
| 92 | 17 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝐽 ∈ (TopOn‘𝑋)) | 
| 93 |  | eltx 23577 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘𝑋)) → ((◡ − “ 𝑢) ∈ (𝐽 ×t 𝐽) ↔ ∀𝑡 ∈ (◡ − “ 𝑢)∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) | 
| 94 | 92, 92, 93 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((◡ − “ 𝑢) ∈ (𝐽 ×t 𝐽) ↔ ∀𝑡 ∈ (◡ − “ 𝑢)∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) | 
| 95 | 91, 94 | mpbid 232 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ∀𝑡 ∈ (◡ − “ 𝑢)∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢))) | 
| 96 |  | ecexg 8750 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ~QG 𝑌) ∈ V → [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌) ∈ V) | 
| 97 | 8, 96 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌) ∈ V | 
| 98 | 66, 97 | fnmpoi 8096 | . . . . . . . . . . . . . . . . . . . . 21
⊢  − Fn
(𝑋 × 𝑋) | 
| 99 |  | elpreima 7077 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ( − Fn
(𝑋 × 𝑋) → (〈𝑎, 𝑏〉 ∈ (◡ − “ 𝑢) ↔ (〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋) ∧ ( − ‘〈𝑎, 𝑏〉) ∈ 𝑢))) | 
| 100 | 98, 99 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑎, 𝑏〉 ∈ (◡ − “ 𝑢) ↔ (〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋) ∧ ( − ‘〈𝑎, 𝑏〉) ∈ 𝑢)) | 
| 101 |  | opelxp 5720 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋) ↔ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) | 
| 102 | 101 | anbi1i 624 | . . . . . . . . . . . . . . . . . . . 20
⊢
((〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋) ∧ ( − ‘〈𝑎, 𝑏〉) ∈ 𝑢) ↔ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ ( − ‘〈𝑎, 𝑏〉) ∈ 𝑢)) | 
| 103 |  | df-ov 7435 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 − 𝑏) = ( − ‘〈𝑎, 𝑏〉) | 
| 104 |  | oveq12 7441 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 = 𝑎 ∧ 𝑤 = 𝑏) → (𝑧(-g‘𝐺)𝑤) = (𝑎(-g‘𝐺)𝑏)) | 
| 105 | 104 | eceq1d 8786 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 = 𝑎 ∧ 𝑤 = 𝑏) → [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) | 
| 106 |  | ecexg 8750 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ~QG 𝑌) ∈ V → [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ V) | 
| 107 | 8, 106 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ V | 
| 108 | 105, 66, 107 | ovmpoa 7589 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑎 − 𝑏) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) | 
| 109 | 103, 108 | eqtr3id 2790 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ( − ‘〈𝑎, 𝑏〉) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) | 
| 110 | 109 | eleq1d 2825 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (( − ‘〈𝑎, 𝑏〉) ∈ 𝑢 ↔ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢)) | 
| 111 | 110 | pm5.32i 574 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ ( − ‘〈𝑎, 𝑏〉) ∈ 𝑢) ↔ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢)) | 
| 112 | 100, 102,
111 | 3bitri 297 | . . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑎, 𝑏〉 ∈ (◡ − “ 𝑢) ↔ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢)) | 
| 113 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 〈𝑎, 𝑏〉 → (𝑡 ∈ (𝑐 × 𝑑) ↔ 〈𝑎, 𝑏〉 ∈ (𝑐 × 𝑑))) | 
| 114 |  | opelxp 5720 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈𝑎, 𝑏〉 ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑)) | 
| 115 | 113, 114 | bitrdi 287 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 〈𝑎, 𝑏〉 → (𝑡 ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑))) | 
| 116 | 115 | anbi1d 631 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 〈𝑎, 𝑏〉 → ((𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) | 
| 117 | 116 | 2rexbidv 3221 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 〈𝑎, 𝑏〉 → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) ↔ ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) | 
| 118 | 117 | rspccv 3618 | . . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑡 ∈
(◡ − “ 𝑢)∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) → (〈𝑎, 𝑏〉 ∈ (◡ − “ 𝑢) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) | 
| 119 | 112, 118 | biimtrrid 243 | . . . . . . . . . . . . . . . . . 18
⊢
(∀𝑡 ∈
(◡ − “ 𝑢)∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) → (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) | 
| 120 | 95, 119 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) | 
| 121 | 65, 120 | mpand 695 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ([(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) | 
| 122 |  | simp-4l 782 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝐺 ∈ TopGrp) | 
| 123 | 57 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑌 ∈ (NrmSGrp‘𝐺)) | 
| 124 |  | simprll 778 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑐 ∈ 𝐽) | 
| 125 | 1, 5, 13, 14, 7 | qustgpopn 24129 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑐 ∈ 𝐽) → (𝐹 “ 𝑐) ∈ 𝐾) | 
| 126 | 122, 123,
124, 125 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹 “ 𝑐) ∈ 𝐾) | 
| 127 |  | simprlr 779 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑑 ∈ 𝐽) | 
| 128 | 1, 5, 13, 14, 7 | qustgpopn 24129 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑑 ∈ 𝐽) → (𝐹 “ 𝑑) ∈ 𝐾) | 
| 129 | 122, 123,
127, 128 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹 “ 𝑑) ∈ 𝐾) | 
| 130 | 58 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑎 ∈ 𝑋) | 
| 131 |  | eceq1 8785 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑎 → [𝑥](𝐺 ~QG 𝑌) = [𝑎](𝐺 ~QG 𝑌)) | 
| 132 | 131, 7, 78 | fvmpt3i 7020 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 ∈ 𝑋 → (𝐹‘𝑎) = [𝑎](𝐺 ~QG 𝑌)) | 
| 133 | 130, 132 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹‘𝑎) = [𝑎](𝐺 ~QG 𝑌)) | 
| 134 | 122, 16 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝐽 ∈ (TopOn‘𝑋)) | 
| 135 |  | toponss 22934 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑐 ∈ 𝐽) → 𝑐 ⊆ 𝑋) | 
| 136 | 134, 124,
135 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑐 ⊆ 𝑋) | 
| 137 |  | simprrl 780 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑)) | 
| 138 | 137 | simpld 494 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑎 ∈ 𝑐) | 
| 139 |  | fnfvima 7254 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 Fn 𝑋 ∧ 𝑐 ⊆ 𝑋 ∧ 𝑎 ∈ 𝑐) → (𝐹‘𝑎) ∈ (𝐹 “ 𝑐)) | 
| 140 | 79, 136, 138, 139 | mp3an2i 1467 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹‘𝑎) ∈ (𝐹 “ 𝑐)) | 
| 141 | 133, 140 | eqeltrrd 2841 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → [𝑎](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑐)) | 
| 142 | 59 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑏 ∈ 𝑋) | 
| 143 |  | eceq1 8785 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑏 → [𝑥](𝐺 ~QG 𝑌) = [𝑏](𝐺 ~QG 𝑌)) | 
| 144 | 143, 7, 78 | fvmpt3i 7020 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 ∈ 𝑋 → (𝐹‘𝑏) = [𝑏](𝐺 ~QG 𝑌)) | 
| 145 | 142, 144 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹‘𝑏) = [𝑏](𝐺 ~QG 𝑌)) | 
| 146 |  | toponss 22934 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑑 ∈ 𝐽) → 𝑑 ⊆ 𝑋) | 
| 147 | 134, 127,
146 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑑 ⊆ 𝑋) | 
| 148 | 137 | simprd 495 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑏 ∈ 𝑑) | 
| 149 |  | fnfvima 7254 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 Fn 𝑋 ∧ 𝑑 ⊆ 𝑋 ∧ 𝑏 ∈ 𝑑) → (𝐹‘𝑏) ∈ (𝐹 “ 𝑑)) | 
| 150 | 79, 147, 148, 149 | mp3an2i 1467 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹‘𝑏) ∈ (𝐹 “ 𝑑)) | 
| 151 | 145, 150 | eqeltrrd 2841 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → [𝑏](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑑)) | 
| 152 | 141, 151 | opelxpd 5723 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑))) | 
| 153 | 136 | sselda 3982 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ 𝑝 ∈ 𝑐) → 𝑝 ∈ 𝑋) | 
| 154 | 147 | sselda 3982 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ 𝑞 ∈ 𝑑) → 𝑞 ∈ 𝑋) | 
| 155 | 153, 154 | anim12dan 619 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) | 
| 156 |  | eceq1 8785 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 𝑝 → [𝑥](𝐺 ~QG 𝑌) = [𝑝](𝐺 ~QG 𝑌)) | 
| 157 | 156, 7, 78 | fvmpt3i 7020 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑝 ∈ 𝑋 → (𝐹‘𝑝) = [𝑝](𝐺 ~QG 𝑌)) | 
| 158 |  | eceq1 8785 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 𝑞 → [𝑥](𝐺 ~QG 𝑌) = [𝑞](𝐺 ~QG 𝑌)) | 
| 159 | 158, 7, 78 | fvmpt3i 7020 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑞 ∈ 𝑋 → (𝐹‘𝑞) = [𝑞](𝐺 ~QG 𝑌)) | 
| 160 |  | opeq12 4874 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐹‘𝑝) = [𝑝](𝐺 ~QG 𝑌) ∧ (𝐹‘𝑞) = [𝑞](𝐺 ~QG 𝑌)) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 = 〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) | 
| 161 | 157, 159,
160 | syl2an 596 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 = 〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) | 
| 162 | 155, 161 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 = 〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) | 
| 163 | 123 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → 𝑌 ∈ (NrmSGrp‘𝐺)) | 
| 164 | 1, 5, 24 | quseccl 19206 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑝 ∈ 𝑋) → [𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)) | 
| 165 | 1, 5, 24 | quseccl 19206 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑞 ∈ 𝑋) → [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)) | 
| 166 | 164, 165 | anim12dan 619 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻))) | 
| 167 | 163, 155,
166 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻))) | 
| 168 |  | opelxpi 5721 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)) → 〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉 ∈ ((Base‘𝐻) × (Base‘𝐻))) | 
| 169 | 167, 168 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → 〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉 ∈ ((Base‘𝐻) × (Base‘𝐻))) | 
| 170 | 1, 5, 60, 27 | qussub 19210 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → ([𝑝](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) | 
| 171 | 170 | 3expb 1120 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ([𝑝](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) | 
| 172 | 163, 155,
171 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ([𝑝](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) | 
| 173 |  | oveq12 7441 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑧 = 𝑝 ∧ 𝑤 = 𝑞) → (𝑧(-g‘𝐺)𝑤) = (𝑝(-g‘𝐺)𝑞)) | 
| 174 | 173 | eceq1d 8786 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑧 = 𝑝 ∧ 𝑤 = 𝑞) → [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) | 
| 175 |  | ecexg 8750 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐺 ~QG 𝑌) ∈ V → [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌) ∈ V) | 
| 176 | 8, 175 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌) ∈ V | 
| 177 | 174, 66, 176 | ovmpoa 7589 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → (𝑝 − 𝑞) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) | 
| 178 | 155, 177 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → (𝑝 − 𝑞) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) | 
| 179 | 172, 178 | eqtr4d 2779 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ([𝑝](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑞](𝐺 ~QG 𝑌)) = (𝑝 − 𝑞)) | 
| 180 |  | df-ov 7435 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ([𝑝](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑞](𝐺 ~QG 𝑌)) = ((-g‘𝐻)‘〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) | 
| 181 |  | df-ov 7435 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑝 − 𝑞) = ( − ‘〈𝑝, 𝑞〉) | 
| 182 | 179, 180,
181 | 3eqtr3g 2799 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ((-g‘𝐻)‘〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) = ( − ‘〈𝑝, 𝑞〉)) | 
| 183 |  | opelxpi 5721 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑) → 〈𝑝, 𝑞〉 ∈ (𝑐 × 𝑑)) | 
| 184 |  | simprrr 781 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) | 
| 185 | 184 | sselda 3982 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ 〈𝑝, 𝑞〉 ∈ (𝑐 × 𝑑)) → 〈𝑝, 𝑞〉 ∈ (◡ − “ 𝑢)) | 
| 186 | 183, 185 | sylan2 593 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → 〈𝑝, 𝑞〉 ∈ (◡ − “ 𝑢)) | 
| 187 |  | elpreima 7077 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ( − Fn
(𝑋 × 𝑋) → (〈𝑝, 𝑞〉 ∈ (◡ − “ 𝑢) ↔ (〈𝑝, 𝑞〉 ∈ (𝑋 × 𝑋) ∧ ( − ‘〈𝑝, 𝑞〉) ∈ 𝑢))) | 
| 188 | 98, 187 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(〈𝑝, 𝑞〉 ∈ (◡ − “ 𝑢) ↔ (〈𝑝, 𝑞〉 ∈ (𝑋 × 𝑋) ∧ ( − ‘〈𝑝, 𝑞〉) ∈ 𝑢)) | 
| 189 | 188 | simprbi 496 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(〈𝑝, 𝑞〉 ∈ (◡ − “ 𝑢) → ( − ‘〈𝑝, 𝑞〉) ∈ 𝑢) | 
| 190 | 186, 189 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ( − ‘〈𝑝, 𝑞〉) ∈ 𝑢) | 
| 191 | 182, 190 | eqeltrd 2840 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ((-g‘𝐻)‘〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) ∈ 𝑢) | 
| 192 | 52, 53 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (-g‘𝐻) Fn ((Base‘𝐻) × (Base‘𝐻))) | 
| 193 | 192 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → (-g‘𝐻) Fn ((Base‘𝐻) × (Base‘𝐻))) | 
| 194 |  | elpreima 7077 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((-g‘𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)) → (〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ (〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧
((-g‘𝐻)‘〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) ∈ 𝑢))) | 
| 195 | 193, 194 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → (〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ (〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧
((-g‘𝐻)‘〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) ∈ 𝑢))) | 
| 196 | 169, 191,
195 | mpbir2and 713 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → 〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢)) | 
| 197 | 162, 196 | eqeltrd 2840 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢)) | 
| 198 | 197 | ralrimivva 3201 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → ∀𝑝 ∈ 𝑐 ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢)) | 
| 199 |  | opeq1 4872 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 = (𝐹‘𝑝) → 〈𝑧, 𝑤〉 = 〈(𝐹‘𝑝), 𝑤〉) | 
| 200 | 199 | eleq1d 2825 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 = (𝐹‘𝑝) → (〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ 〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢))) | 
| 201 | 200 | ralbidv 3177 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = (𝐹‘𝑝) → (∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢))) | 
| 202 | 201 | ralima 7258 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹 Fn 𝑋 ∧ 𝑐 ⊆ 𝑋) → (∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑝 ∈ 𝑐 ∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢))) | 
| 203 | 79, 202 | mpan 690 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 ⊆ 𝑋 → (∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑝 ∈ 𝑐 ∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢))) | 
| 204 |  | opeq2 4873 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 = (𝐹‘𝑞) → 〈(𝐹‘𝑝), 𝑤〉 = 〈(𝐹‘𝑝), (𝐹‘𝑞)〉) | 
| 205 | 204 | eleq1d 2825 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 = (𝐹‘𝑞) → (〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) | 
| 206 | 205 | ralima 7258 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹 Fn 𝑋 ∧ 𝑑 ⊆ 𝑋) → (∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) | 
| 207 | 79, 206 | mpan 690 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑑 ⊆ 𝑋 → (∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) | 
| 208 | 207 | ralbidv 3177 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑑 ⊆ 𝑋 → (∀𝑝 ∈ 𝑐 ∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑝 ∈ 𝑐 ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) | 
| 209 | 203, 208 | sylan9bb 509 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑐 ⊆ 𝑋 ∧ 𝑑 ⊆ 𝑋) → (∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑝 ∈ 𝑐 ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) | 
| 210 | 136, 147,
209 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑝 ∈ 𝑐 ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) | 
| 211 | 198, 210 | mpbird 257 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → ∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢)) | 
| 212 |  | dfss3 3971 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑦 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑))𝑦 ∈ (◡(-g‘𝐻) “ 𝑢)) | 
| 213 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 〈𝑧, 𝑤〉 → (𝑦 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ 〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢))) | 
| 214 | 213 | ralxp 5851 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑦 ∈
((𝐹 “ 𝑐) × (𝐹 “ 𝑑))𝑦 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢)) | 
| 215 | 212, 214 | bitri 275 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢)) | 
| 216 | 211, 215 | sylibr 234 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢)) | 
| 217 |  | xpeq1 5698 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑟 = (𝐹 “ 𝑐) → (𝑟 × 𝑠) = ((𝐹 “ 𝑐) × 𝑠)) | 
| 218 | 217 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 = (𝐹 “ 𝑐) → (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ↔ 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × 𝑠))) | 
| 219 | 217 | sseq1d 4014 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 = (𝐹 “ 𝑐) → ((𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢) ↔ ((𝐹 “ 𝑐) × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) | 
| 220 | 218, 219 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 = (𝐹 “ 𝑐) → ((〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)) ↔ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × 𝑠) ∧ ((𝐹 “ 𝑐) × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) | 
| 221 |  | xpeq2 5705 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 = (𝐹 “ 𝑑) → ((𝐹 “ 𝑐) × 𝑠) = ((𝐹 “ 𝑐) × (𝐹 “ 𝑑))) | 
| 222 | 221 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = (𝐹 “ 𝑑) → (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × 𝑠) ↔ 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)))) | 
| 223 | 221 | sseq1d 4014 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = (𝐹 “ 𝑑) → (((𝐹 “ 𝑐) × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢) ↔ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢))) | 
| 224 | 222, 223 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = (𝐹 “ 𝑑) → ((〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × 𝑠) ∧ ((𝐹 “ 𝑐) × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)) ↔ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ∧ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢)))) | 
| 225 | 220, 224 | rspc2ev 3634 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹 “ 𝑐) ∈ 𝐾 ∧ (𝐹 “ 𝑑) ∈ 𝐾 ∧ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ∧ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢))) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) | 
| 226 | 126, 129,
152, 216, 225 | syl112anc 1375 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) | 
| 227 | 226 | expr 456 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) | 
| 228 | 227 | rexlimdvva 3212 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) | 
| 229 | 121, 228 | syld 47 | . . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ([(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢 → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) | 
| 230 | 64, 229 | sylbid 240 | . . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) ∈ 𝑢 → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) | 
| 231 | 230 | adantld 490 | . . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧
((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) ∈ 𝑢) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) | 
| 232 | 55, 231 | sylbid 240 | . . . . . . . . . . . 12
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) | 
| 233 |  | opeq12 4874 | . . . . . . . . . . . . . 14
⊢ ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → 〈𝑥, 𝑦〉 = 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) | 
| 234 | 233 | eleq1d 2825 | . . . . . . . . . . . . 13
⊢ ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) | 
| 235 | 233 | eleq1d 2825 | . . . . . . . . . . . . . 14
⊢ ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))} ↔ 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))})) | 
| 236 |  | opex 5468 | . . . . . . . . . . . . . . 15
⊢
〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ V | 
| 237 |  | eleq1 2828 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 → (𝑤 ∈ (𝑟 × 𝑠) ↔ 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠))) | 
| 238 | 237 | anbi1d 631 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 = 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 → ((𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)) ↔ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) | 
| 239 | 238 | 2rexbidv 3221 | . . . . . . . . . . . . . . 15
⊢ (𝑤 = 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 → (∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)) ↔ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) | 
| 240 | 236, 239 | elab 3678 | . . . . . . . . . . . . . 14
⊢
(〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))} ↔ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) | 
| 241 | 235, 240 | bitrdi 287 | . . . . . . . . . . . . 13
⊢ ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))} ↔ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) | 
| 242 | 234, 241 | imbi12d 344 | . . . . . . . . . . . 12
⊢ ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → ((〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → 〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))}) ↔ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))))) | 
| 243 | 232, 242 | syl5ibrcom 247 | . . . . . . . . . . 11
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → 〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))}))) | 
| 244 | 243 | rexlimdvva 3212 | . . . . . . . . . 10
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → 〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))}))) | 
| 245 | 50, 244 | sylbird 260 | . . . . . . . . 9
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (〈𝑥, 𝑦〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → 〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))}))) | 
| 246 | 245 | com23 86 | . . . . . . . 8
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → (〈𝑥, 𝑦〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) → 〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))}))) | 
| 247 | 37, 246 | mpdd 43 | . . . . . . 7
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → 〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))})) | 
| 248 | 36, 247 | relssdv 5797 | . . . . . 6
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (◡(-g‘𝐻) “ 𝑢) ⊆ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))}) | 
| 249 |  | ssabral 4064 | . . . . . 6
⊢ ((◡(-g‘𝐻) “ 𝑢) ⊆ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))} ↔ ∀𝑤 ∈ (◡(-g‘𝐻) “ 𝑢)∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) | 
| 250 | 248, 249 | sylib 218 | . . . . 5
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → ∀𝑤 ∈ (◡(-g‘𝐻) “ 𝑢)∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) | 
| 251 |  | eltx 23577 | . . . . . . 7
⊢ ((𝐾 ∈
(TopOn‘(Base‘𝐻)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → ((◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ (◡(-g‘𝐻) “ 𝑢)∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) | 
| 252 | 23, 23, 251 | syl2anc 584 | . . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ((◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ (◡(-g‘𝐻) “ 𝑢)∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) | 
| 253 | 252 | adantr 480 | . . . . 5
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → ((◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ (◡(-g‘𝐻) “ 𝑢)∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) | 
| 254 | 250, 253 | mpbird 257 | . . . 4
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾)) | 
| 255 | 254 | ralrimiva 3145 | . . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ∀𝑢 ∈ 𝐾 (◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾)) | 
| 256 |  | txtopon 23600 | . . . . 5
⊢ ((𝐾 ∈
(TopOn‘(Base‘𝐻)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → (𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻)))) | 
| 257 | 23, 23, 256 | syl2anc 584 | . . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻)))) | 
| 258 |  | iscn 23244 | . . . 4
⊢ (((𝐾 ×t 𝐾) ∈
(TopOn‘((Base‘𝐻) × (Base‘𝐻))) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) →
((-g‘𝐻)
∈ ((𝐾
×t 𝐾) Cn
𝐾) ↔
((-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) ∧ ∀𝑢 ∈ 𝐾 (◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾)))) | 
| 259 | 257, 23, 258 | syl2anc 584 | . . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
((-g‘𝐻)
∈ ((𝐾
×t 𝐾) Cn
𝐾) ↔
((-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) ∧ ∀𝑢 ∈ 𝐾 (◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾)))) | 
| 260 | 29, 255, 259 | mpbir2and 713 | . 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
(-g‘𝐻)
∈ ((𝐾
×t 𝐾) Cn
𝐾)) | 
| 261 | 14, 27 | istgp2 24100 | . 2
⊢ (𝐻 ∈ TopGrp ↔ (𝐻 ∈ Grp ∧ 𝐻 ∈ TopSp ∧
(-g‘𝐻)
∈ ((𝐾
×t 𝐾) Cn
𝐾))) | 
| 262 | 3, 26, 260, 261 | syl3anbrc 1343 | 1
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopGrp) |