Step | Hyp | Ref
| Expression |
1 | | qustgp.h |
. . . 4
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌)) |
2 | 1 | qusgrp 17857 |
. . 3
⊢ (𝑌 ∈ (NrmSGrp‘𝐺) → 𝐻 ∈ Grp) |
3 | 2 | adantl 467 |
. 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 6823 |
. . . . . . . 8
⊢ (𝐺 ~QG 𝑌) ∈ V |
9 | 8 | a1i 11 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐺 ~QG 𝑌) ∈ V) |
10 | | simpl 468 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐺 ∈ TopGrp) |
11 | 4, 6, 7, 9, 10 | qusval 16410 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 = (𝐹 “s 𝐺)) |
12 | 4, 6, 7, 9, 10 | quslem 16411 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹:𝑋–onto→(𝑋 / (𝐺 ~QG 𝑌))) |
13 | | qustgpopn.j |
. . . . . 6
⊢ 𝐽 = (TopOpen‘𝐺) |
14 | | qustgpopn.k |
. . . . . 6
⊢ 𝐾 = (TopOpen‘𝐻) |
15 | 11, 6, 12, 10, 13, 14 | imastopn 21744 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 = (𝐽 qTop 𝐹)) |
16 | 13, 5 | tgptopon 22106 |
. . . . . . 7
⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋)) |
17 | 16 | adantr 466 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐽 ∈ (TopOn‘𝑋)) |
18 | | qtoptopon 21728 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→(𝑋 / (𝐺 ~QG 𝑌))) → (𝐽 qTop 𝐹) ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌)))) |
19 | 17, 12, 18 | syl2anc 573 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐽 qTop 𝐹) ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌)))) |
20 | 15, 19 | eqeltrd 2850 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌)))) |
21 | 4, 6, 9, 10 | qusbas 16413 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑋 / (𝐺 ~QG 𝑌)) = (Base‘𝐻)) |
22 | 21 | fveq2d 6336 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))) = (TopOn‘(Base‘𝐻))) |
23 | 20, 22 | eleqtrd 2852 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 ∈ (TopOn‘(Base‘𝐻))) |
24 | | eqid 2771 |
. . . 4
⊢
(Base‘𝐻) =
(Base‘𝐻) |
25 | 24, 14 | istps 20959 |
. . 3
⊢ (𝐻 ∈ TopSp ↔ 𝐾 ∈
(TopOn‘(Base‘𝐻))) |
26 | 23, 25 | sylibr 224 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopSp) |
27 | | eqid 2771 |
. . . . 5
⊢
(-g‘𝐻) = (-g‘𝐻) |
28 | 24, 27 | grpsubf 17702 |
. . . 4
⊢ (𝐻 ∈ Grp →
(-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻)) |
29 | 3, 28 | syl 17 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
(-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻)) |
30 | | cnvimass 5626 |
. . . . . . . . 9
⊢ (◡(-g‘𝐻) “ 𝑢) ⊆ dom (-g‘𝐻) |
31 | | fdm 6191 |
. . . . . . . . . . 11
⊢
((-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) → dom (-g‘𝐻) = ((Base‘𝐻) × (Base‘𝐻))) |
32 | 29, 31 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → dom
(-g‘𝐻) =
((Base‘𝐻) ×
(Base‘𝐻))) |
33 | 32 | adantr 466 |
. . . . . . . . 9
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → dom (-g‘𝐻) = ((Base‘𝐻) × (Base‘𝐻))) |
34 | 30, 33 | syl5sseq 3802 |
. . . . . . . 8
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (◡(-g‘𝐻) “ 𝑢) ⊆ ((Base‘𝐻) × (Base‘𝐻))) |
35 | | relxp 5266 |
. . . . . . . 8
⊢ Rel
((Base‘𝐻) ×
(Base‘𝐻)) |
36 | | relss 5346 |
. . . . . . . 8
⊢ ((◡(-g‘𝐻) “ 𝑢) ⊆ ((Base‘𝐻) × (Base‘𝐻)) → (Rel ((Base‘𝐻) × (Base‘𝐻)) → Rel (◡(-g‘𝐻) “ 𝑢))) |
37 | 34, 35, 36 | mpisyl 21 |
. . . . . . 7
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → Rel (◡(-g‘𝐻) “ 𝑢)) |
38 | 34 | sseld 3751 |
. . . . . . . 8
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → 〈𝑥, 𝑦〉 ∈ ((Base‘𝐻) × (Base‘𝐻)))) |
39 | | vex 3354 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
40 | 39 | elqs 7951 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ ∃𝑎 ∈ 𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌)) |
41 | 21 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (𝑋 / (𝐺 ~QG 𝑌)) = (Base‘𝐻)) |
42 | 41 | eleq2d 2836 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (𝑥 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ 𝑥 ∈ (Base‘𝐻))) |
43 | 40, 42 | syl5bbr 274 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (∃𝑎 ∈ 𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ↔ 𝑥 ∈ (Base‘𝐻))) |
44 | | vex 3354 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V |
45 | 44 | elqs 7951 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ ∃𝑏 ∈ 𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌)) |
46 | 41 | eleq2d 2836 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (𝑦 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ 𝑦 ∈ (Base‘𝐻))) |
47 | 45, 46 | syl5bbr 274 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (∃𝑏 ∈ 𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌) ↔ 𝑦 ∈ (Base‘𝐻))) |
48 | 43, 47 | anbi12d 616 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → ((∃𝑎 ∈ 𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ ∃𝑏 ∈ 𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻)))) |
49 | | reeanv 3255 |
. . . . . . . . . . 11
⊢
(∃𝑎 ∈
𝑋 ∃𝑏 ∈ 𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ (∃𝑎 ∈ 𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ ∃𝑏 ∈ 𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌))) |
50 | | opelxp 5286 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) |
51 | 48, 49, 50 | 3bitr4g 303 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ 〈𝑥, 𝑦〉 ∈ ((Base‘𝐻) × (Base‘𝐻)))) |
52 | 3 | ad2antrr 705 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝐻 ∈ Grp) |
53 | 52, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻)) |
54 | | ffn 6185 |
. . . . . . . . . . . . . 14
⊢
((-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) → (-g‘𝐻) Fn ((Base‘𝐻) × (Base‘𝐻))) |
55 | | elpreima 6480 |
. . . . . . . . . . . . . 14
⊢
((-g‘𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)) → (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧
((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) ∈ 𝑢))) |
56 | 53, 54, 55 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧
((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) ∈ 𝑢))) |
57 | | df-ov 6796 |
. . . . . . . . . . . . . . . . 17
⊢ ([𝑎](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑏](𝐺 ~QG 𝑌)) = ((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) |
58 | | simpllr 760 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑌 ∈ (NrmSGrp‘𝐺)) |
59 | | simprl 754 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑎 ∈ 𝑋) |
60 | | simprr 756 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑏 ∈ 𝑋) |
61 | | eqid 2771 |
. . . . . . . . . . . . . . . . . . 19
⊢
(-g‘𝐺) = (-g‘𝐺) |
62 | 1, 5, 61, 27 | qussub 17862 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ([𝑎](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑏](𝐺 ~QG 𝑌)) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) |
63 | 58, 59, 60, 62 | syl3anc 1476 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ([𝑎](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑏](𝐺 ~QG 𝑌)) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) |
64 | 57, 63 | syl5eqr 2819 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) |
65 | 64 | eleq1d 2835 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) ∈ 𝑢 ↔ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢)) |
66 | | simpr 471 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) |
67 | | qustgplem.m |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ − =
(𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌)) |
68 | | tgpgrp 22102 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
69 | 68 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐺 ∈ Grp) |
70 | 5, 61 | grpsubf 17702 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐺 ∈ Grp →
(-g‘𝐺):(𝑋 × 𝑋)⟶𝑋) |
71 | | ffn 6185 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((-g‘𝐺):(𝑋 × 𝑋)⟶𝑋 → (-g‘𝐺) Fn (𝑋 × 𝑋)) |
72 | 69, 70, 71 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
(-g‘𝐺) Fn
(𝑋 × 𝑋)) |
73 | | fnov 6915 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((-g‘𝐺) Fn (𝑋 × 𝑋) ↔ (-g‘𝐺) = (𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ (𝑧(-g‘𝐺)𝑤))) |
74 | 72, 73 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
(-g‘𝐺) =
(𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ (𝑧(-g‘𝐺)𝑤))) |
75 | 13, 61 | tgpsubcn 22114 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐺 ∈ TopGrp →
(-g‘𝐺)
∈ ((𝐽
×t 𝐽) Cn
𝐽)) |
76 | 75 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
(-g‘𝐺)
∈ ((𝐽
×t 𝐽) Cn
𝐽)) |
77 | 74, 76 | eqeltrrd 2851 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ (𝑧(-g‘𝐺)𝑤)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
78 | | ecexg 7900 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐺 ~QG 𝑌) ∈ V → [𝑥](𝐺 ~QG 𝑌) ∈ V) |
79 | 8, 78 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ [𝑥](𝐺 ~QG 𝑌) ∈ V |
80 | 79, 7 | fnmpti 6162 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝐹 Fn 𝑋 |
81 | | qtopid 21729 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 Fn 𝑋) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))) |
82 | 17, 80, 81 | sylancl 574 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))) |
83 | 15 | oveq2d 6809 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐽 Cn 𝐾) = (𝐽 Cn (𝐽 qTop 𝐹))) |
84 | 82, 83 | eleqtrrd 2853 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
85 | 7, 84 | syl5eqelr 2855 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑥 ∈ 𝑋 ↦ [𝑥](𝐺 ~QG 𝑌)) ∈ (𝐽 Cn 𝐾)) |
86 | | eceq1 7934 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = (𝑧(-g‘𝐺)𝑤) → [𝑥](𝐺 ~QG 𝑌) = [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌)) |
87 | 17, 17, 77, 17, 85, 86 | cnmpt21 21695 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌)) ∈ ((𝐽 ×t 𝐽) Cn 𝐾)) |
88 | 67, 87 | syl5eqel 2854 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → − ∈ ((𝐽 ×t 𝐽) Cn 𝐾)) |
89 | 88 | ad2antrr 705 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → − ∈ ((𝐽 ×t 𝐽) Cn 𝐾)) |
90 | | simplr 752 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑢 ∈ 𝐾) |
91 | | cnima 21290 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (( − ∈
((𝐽 ×t
𝐽) Cn 𝐾) ∧ 𝑢 ∈ 𝐾) → (◡ − “ 𝑢) ∈ (𝐽 ×t 𝐽)) |
92 | 89, 90, 91 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (◡ − “ 𝑢) ∈ (𝐽 ×t 𝐽)) |
93 | 17 | ad2antrr 705 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝐽 ∈ (TopOn‘𝑋)) |
94 | | eltx 21592 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘𝑋)) → ((◡ − “ 𝑢) ∈ (𝐽 ×t 𝐽) ↔ ∀𝑡 ∈ (◡ − “ 𝑢)∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) |
95 | 93, 93, 94 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((◡ − “ 𝑢) ∈ (𝐽 ×t 𝐽) ↔ ∀𝑡 ∈ (◡ − “ 𝑢)∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) |
96 | 92, 95 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ∀𝑡 ∈ (◡ − “ 𝑢)∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢))) |
97 | | ecexg 7900 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ~QG 𝑌) ∈ V → [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌) ∈ V) |
98 | 8, 97 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌) ∈ V |
99 | 67, 98 | fnmpt2i 7389 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ − Fn
(𝑋 × 𝑋) |
100 | | elpreima 6480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ( − Fn
(𝑋 × 𝑋) → (〈𝑎, 𝑏〉 ∈ (◡ − “ 𝑢) ↔ (〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋) ∧ ( − ‘〈𝑎, 𝑏〉) ∈ 𝑢))) |
101 | 99, 100 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑎, 𝑏〉 ∈ (◡ − “ 𝑢) ↔ (〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋) ∧ ( − ‘〈𝑎, 𝑏〉) ∈ 𝑢)) |
102 | | opelxp 5286 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋) ↔ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) |
103 | 102 | anbi1i 610 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋) ∧ ( − ‘〈𝑎, 𝑏〉) ∈ 𝑢) ↔ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ ( − ‘〈𝑎, 𝑏〉) ∈ 𝑢)) |
104 | | df-ov 6796 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 − 𝑏) = ( − ‘〈𝑎, 𝑏〉) |
105 | | oveq12 6802 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 = 𝑎 ∧ 𝑤 = 𝑏) → (𝑧(-g‘𝐺)𝑤) = (𝑎(-g‘𝐺)𝑏)) |
106 | 105 | eceq1d 7935 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 = 𝑎 ∧ 𝑤 = 𝑏) → [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) |
107 | | ecexg 7900 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ~QG 𝑌) ∈ V → [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ V) |
108 | 8, 107 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ V |
109 | 106, 67, 108 | ovmpt2a 6938 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑎 − 𝑏) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) |
110 | 104, 109 | syl5eqr 2819 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ( − ‘〈𝑎, 𝑏〉) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) |
111 | 110 | eleq1d 2835 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (( − ‘〈𝑎, 𝑏〉) ∈ 𝑢 ↔ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢)) |
112 | 111 | pm5.32i 564 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ ( − ‘〈𝑎, 𝑏〉) ∈ 𝑢) ↔ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢)) |
113 | 101, 103,
112 | 3bitri 286 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑎, 𝑏〉 ∈ (◡ − “ 𝑢) ↔ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢)) |
114 | | eleq1 2838 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 〈𝑎, 𝑏〉 → (𝑡 ∈ (𝑐 × 𝑑) ↔ 〈𝑎, 𝑏〉 ∈ (𝑐 × 𝑑))) |
115 | | opelxp 5286 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈𝑎, 𝑏〉 ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑)) |
116 | 114, 115 | syl6bb 276 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 〈𝑎, 𝑏〉 → (𝑡 ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑))) |
117 | 116 | anbi1d 615 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 〈𝑎, 𝑏〉 → ((𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) |
118 | 117 | 2rexbidv 3205 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 〈𝑎, 𝑏〉 → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) ↔ ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) |
119 | 118 | rspccv 3457 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑡 ∈
(◡ − “ 𝑢)∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) → (〈𝑎, 𝑏〉 ∈ (◡ − “ 𝑢) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) |
120 | 113, 119 | syl5bir 233 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑡 ∈
(◡ − “ 𝑢)∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) → (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) |
121 | 96, 120 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) |
122 | 66, 121 | mpand 675 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ([(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) |
123 | | simp-4l 768 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝐺 ∈ TopGrp) |
124 | 58 | adantr 466 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑌 ∈ (NrmSGrp‘𝐺)) |
125 | | simprll 764 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑐 ∈ 𝐽) |
126 | 1, 5, 13, 14, 7 | qustgpopn 22143 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑐 ∈ 𝐽) → (𝐹 “ 𝑐) ∈ 𝐾) |
127 | 123, 124,
125, 126 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹 “ 𝑐) ∈ 𝐾) |
128 | | simprlr 765 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑑 ∈ 𝐽) |
129 | 1, 5, 13, 14, 7 | qustgpopn 22143 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑑 ∈ 𝐽) → (𝐹 “ 𝑑) ∈ 𝐾) |
130 | 123, 124,
128, 129 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹 “ 𝑑) ∈ 𝐾) |
131 | 59 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑎 ∈ 𝑋) |
132 | | eceq1 7934 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑎 → [𝑥](𝐺 ~QG 𝑌) = [𝑎](𝐺 ~QG 𝑌)) |
133 | 132, 7, 79 | fvmpt3i 6429 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 ∈ 𝑋 → (𝐹‘𝑎) = [𝑎](𝐺 ~QG 𝑌)) |
134 | 131, 133 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹‘𝑎) = [𝑎](𝐺 ~QG 𝑌)) |
135 | 123, 16 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝐽 ∈ (TopOn‘𝑋)) |
136 | | toponss 20952 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑐 ∈ 𝐽) → 𝑐 ⊆ 𝑋) |
137 | 135, 125,
136 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑐 ⊆ 𝑋) |
138 | | simprrl 766 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑)) |
139 | 138 | simpld 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑎 ∈ 𝑐) |
140 | | fnfvima 6639 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹 Fn 𝑋 ∧ 𝑐 ⊆ 𝑋 ∧ 𝑎 ∈ 𝑐) → (𝐹‘𝑎) ∈ (𝐹 “ 𝑐)) |
141 | 80, 140 | mp3an1 1559 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑐 ⊆ 𝑋 ∧ 𝑎 ∈ 𝑐) → (𝐹‘𝑎) ∈ (𝐹 “ 𝑐)) |
142 | 137, 139,
141 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹‘𝑎) ∈ (𝐹 “ 𝑐)) |
143 | 134, 142 | eqeltrrd 2851 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → [𝑎](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑐)) |
144 | 60 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑏 ∈ 𝑋) |
145 | | eceq1 7934 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑏 → [𝑥](𝐺 ~QG 𝑌) = [𝑏](𝐺 ~QG 𝑌)) |
146 | 145, 7, 79 | fvmpt3i 6429 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 ∈ 𝑋 → (𝐹‘𝑏) = [𝑏](𝐺 ~QG 𝑌)) |
147 | 144, 146 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹‘𝑏) = [𝑏](𝐺 ~QG 𝑌)) |
148 | | toponss 20952 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑑 ∈ 𝐽) → 𝑑 ⊆ 𝑋) |
149 | 135, 128,
148 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑑 ⊆ 𝑋) |
150 | 138 | simprd 483 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑏 ∈ 𝑑) |
151 | | fnfvima 6639 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹 Fn 𝑋 ∧ 𝑑 ⊆ 𝑋 ∧ 𝑏 ∈ 𝑑) → (𝐹‘𝑏) ∈ (𝐹 “ 𝑑)) |
152 | 80, 151 | mp3an1 1559 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑑 ⊆ 𝑋 ∧ 𝑏 ∈ 𝑑) → (𝐹‘𝑏) ∈ (𝐹 “ 𝑑)) |
153 | 149, 150,
152 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹‘𝑏) ∈ (𝐹 “ 𝑑)) |
154 | 147, 153 | eqeltrrd 2851 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → [𝑏](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑑)) |
155 | | opelxpi 5288 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (([𝑎](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑐) ∧ [𝑏](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑑)) → 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑))) |
156 | 143, 154,
155 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑))) |
157 | 137 | sselda 3752 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ 𝑝 ∈ 𝑐) → 𝑝 ∈ 𝑋) |
158 | 149 | sselda 3752 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ 𝑞 ∈ 𝑑) → 𝑞 ∈ 𝑋) |
159 | 157, 158 | anim12dan 605 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) |
160 | | eceq1 7934 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 𝑝 → [𝑥](𝐺 ~QG 𝑌) = [𝑝](𝐺 ~QG 𝑌)) |
161 | 160, 7, 79 | fvmpt3i 6429 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑝 ∈ 𝑋 → (𝐹‘𝑝) = [𝑝](𝐺 ~QG 𝑌)) |
162 | | eceq1 7934 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 𝑞 → [𝑥](𝐺 ~QG 𝑌) = [𝑞](𝐺 ~QG 𝑌)) |
163 | 162, 7, 79 | fvmpt3i 6429 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑞 ∈ 𝑋 → (𝐹‘𝑞) = [𝑞](𝐺 ~QG 𝑌)) |
164 | | opeq12 4541 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐹‘𝑝) = [𝑝](𝐺 ~QG 𝑌) ∧ (𝐹‘𝑞) = [𝑞](𝐺 ~QG 𝑌)) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 = 〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) |
165 | 161, 163,
164 | syl2an 583 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 = 〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) |
166 | 159, 165 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 = 〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) |
167 | 124 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → 𝑌 ∈ (NrmSGrp‘𝐺)) |
168 | 1, 5, 24 | quseccl 17858 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑝 ∈ 𝑋) → [𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)) |
169 | 1, 5, 24 | quseccl 17858 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑞 ∈ 𝑋) → [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)) |
170 | 168, 169 | anim12dan 605 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻))) |
171 | 167, 159,
170 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻))) |
172 | | opelxpi 5288 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)) → 〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉 ∈ ((Base‘𝐻) × (Base‘𝐻))) |
173 | 171, 172 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → 〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉 ∈ ((Base‘𝐻) × (Base‘𝐻))) |
174 | 1, 5, 61, 27 | qussub 17862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → ([𝑝](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) |
175 | 174 | 3expb 1113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ([𝑝](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) |
176 | 167, 159,
175 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ([𝑝](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) |
177 | | oveq12 6802 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑧 = 𝑝 ∧ 𝑤 = 𝑞) → (𝑧(-g‘𝐺)𝑤) = (𝑝(-g‘𝐺)𝑞)) |
178 | 177 | eceq1d 7935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑧 = 𝑝 ∧ 𝑤 = 𝑞) → [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) |
179 | | ecexg 7900 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐺 ~QG 𝑌) ∈ V → [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌) ∈ V) |
180 | 8, 179 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌) ∈ V |
181 | 178, 67, 180 | ovmpt2a 6938 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → (𝑝 − 𝑞) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) |
182 | 159, 181 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → (𝑝 − 𝑞) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) |
183 | 176, 182 | eqtr4d 2808 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ([𝑝](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑞](𝐺 ~QG 𝑌)) = (𝑝 − 𝑞)) |
184 | | df-ov 6796 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ([𝑝](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑞](𝐺 ~QG 𝑌)) = ((-g‘𝐻)‘〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) |
185 | | df-ov 6796 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑝 − 𝑞) = ( − ‘〈𝑝, 𝑞〉) |
186 | 183, 184,
185 | 3eqtr3g 2828 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ((-g‘𝐻)‘〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) = ( − ‘〈𝑝, 𝑞〉)) |
187 | | opelxpi 5288 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑) → 〈𝑝, 𝑞〉 ∈ (𝑐 × 𝑑)) |
188 | | simprrr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) |
189 | 188 | sselda 3752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ 〈𝑝, 𝑞〉 ∈ (𝑐 × 𝑑)) → 〈𝑝, 𝑞〉 ∈ (◡ − “ 𝑢)) |
190 | 187, 189 | sylan2 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → 〈𝑝, 𝑞〉 ∈ (◡ − “ 𝑢)) |
191 | | elpreima 6480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ( − Fn
(𝑋 × 𝑋) → (〈𝑝, 𝑞〉 ∈ (◡ − “ 𝑢) ↔ (〈𝑝, 𝑞〉 ∈ (𝑋 × 𝑋) ∧ ( − ‘〈𝑝, 𝑞〉) ∈ 𝑢))) |
192 | 99, 191 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(〈𝑝, 𝑞〉 ∈ (◡ − “ 𝑢) ↔ (〈𝑝, 𝑞〉 ∈ (𝑋 × 𝑋) ∧ ( − ‘〈𝑝, 𝑞〉) ∈ 𝑢)) |
193 | 192 | simprbi 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(〈𝑝, 𝑞〉 ∈ (◡ − “ 𝑢) → ( − ‘〈𝑝, 𝑞〉) ∈ 𝑢) |
194 | 190, 193 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ( − ‘〈𝑝, 𝑞〉) ∈ 𝑢) |
195 | 186, 194 | eqeltrd 2850 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ((-g‘𝐻)‘〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) ∈ 𝑢) |
196 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (-g‘𝐻) Fn ((Base‘𝐻) × (Base‘𝐻))) |
197 | 196 | ad2antrr 705 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → (-g‘𝐻) Fn ((Base‘𝐻) × (Base‘𝐻))) |
198 | | elpreima 6480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((-g‘𝐻) Fn ((Base‘𝐻) × (Base‘𝐻)) → (〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ (〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧
((-g‘𝐻)‘〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) ∈ 𝑢))) |
199 | 197, 198 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → (〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ (〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧
((-g‘𝐻)‘〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) ∈ 𝑢))) |
200 | 173, 195,
199 | mpbir2and 692 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → 〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢)) |
201 | 166, 200 | eqeltrd 2850 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢)) |
202 | 201 | ralrimivva 3120 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → ∀𝑝 ∈ 𝑐 ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢)) |
203 | | opeq1 4539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 = (𝐹‘𝑝) → 〈𝑧, 𝑤〉 = 〈(𝐹‘𝑝), 𝑤〉) |
204 | 203 | eleq1d 2835 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 = (𝐹‘𝑝) → (〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ 〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
205 | 204 | ralbidv 3135 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = (𝐹‘𝑝) → (∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
206 | 205 | ralima 6641 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹 Fn 𝑋 ∧ 𝑐 ⊆ 𝑋) → (∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑝 ∈ 𝑐 ∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
207 | 80, 206 | mpan 670 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 ⊆ 𝑋 → (∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑝 ∈ 𝑐 ∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
208 | | opeq2 4540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 = (𝐹‘𝑞) → 〈(𝐹‘𝑝), 𝑤〉 = 〈(𝐹‘𝑝), (𝐹‘𝑞)〉) |
209 | 208 | eleq1d 2835 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 = (𝐹‘𝑞) → (〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
210 | 209 | ralima 6641 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹 Fn 𝑋 ∧ 𝑑 ⊆ 𝑋) → (∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
211 | 80, 210 | mpan 670 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑑 ⊆ 𝑋 → (∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
212 | 211 | ralbidv 3135 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑑 ⊆ 𝑋 → (∀𝑝 ∈ 𝑐 ∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑝 ∈ 𝑐 ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
213 | 207, 212 | sylan9bb 499 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑐 ⊆ 𝑋 ∧ 𝑑 ⊆ 𝑋) → (∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑝 ∈ 𝑐 ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
214 | 137, 149,
213 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑝 ∈ 𝑐 ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
215 | 202, 214 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → ∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢)) |
216 | | dfss3 3741 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑦 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑))𝑦 ∈ (◡(-g‘𝐻) “ 𝑢)) |
217 | | eleq1 2838 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 〈𝑧, 𝑤〉 → (𝑦 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ 〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
218 | 217 | ralxp 5402 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑦 ∈
((𝐹 “ 𝑐) × (𝐹 “ 𝑑))𝑦 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢)) |
219 | 216, 218 | bitri 264 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢)) |
220 | 215, 219 | sylibr 224 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢)) |
221 | | xpeq1 5263 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑟 = (𝐹 “ 𝑐) → (𝑟 × 𝑠) = ((𝐹 “ 𝑐) × 𝑠)) |
222 | 221 | eleq2d 2836 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 = (𝐹 “ 𝑐) → (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ↔ 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × 𝑠))) |
223 | 221 | sseq1d 3781 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 = (𝐹 “ 𝑐) → ((𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢) ↔ ((𝐹 “ 𝑐) × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) |
224 | 222, 223 | anbi12d 616 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 = (𝐹 “ 𝑐) → ((〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)) ↔ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × 𝑠) ∧ ((𝐹 “ 𝑐) × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
225 | | xpeq2 5269 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 = (𝐹 “ 𝑑) → ((𝐹 “ 𝑐) × 𝑠) = ((𝐹 “ 𝑐) × (𝐹 “ 𝑑))) |
226 | 225 | eleq2d 2836 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = (𝐹 “ 𝑑) → (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × 𝑠) ↔ 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)))) |
227 | 225 | sseq1d 3781 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = (𝐹 “ 𝑑) → (((𝐹 “ 𝑐) × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢) ↔ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢))) |
228 | 226, 227 | anbi12d 616 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = (𝐹 “ 𝑑) → ((〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × 𝑠) ∧ ((𝐹 “ 𝑐) × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)) ↔ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ∧ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
229 | 224, 228 | rspc2ev 3474 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹 “ 𝑐) ∈ 𝐾 ∧ (𝐹 “ 𝑑) ∈ 𝐾 ∧ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ∧ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢))) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) |
230 | 127, 130,
156, 220, 229 | syl112anc 1480 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) |
231 | 230 | expr 444 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
232 | 231 | rexlimdvva 3186 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
233 | 122, 232 | syld 47 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ([(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢 → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
234 | 65, 233 | sylbid 230 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) ∈ 𝑢 → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
235 | 234 | adantld 478 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧
((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) ∈ 𝑢) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
236 | 56, 235 | sylbid 230 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
237 | | opeq12 4541 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → 〈𝑥, 𝑦〉 = 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) |
238 | 237 | eleq1d 2835 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
239 | 237 | eleq1d 2835 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))} ↔ 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))})) |
240 | | opex 5060 |
. . . . . . . . . . . . . . 15
⊢
〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ V |
241 | | eleq1 2838 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 → (𝑤 ∈ (𝑟 × 𝑠) ↔ 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠))) |
242 | 241 | anbi1d 615 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 → ((𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)) ↔ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
243 | 242 | 2rexbidv 3205 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 → (∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)) ↔ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
244 | 240, 243 | elab 3501 |
. . . . . . . . . . . . . 14
⊢
(〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))} ↔ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) |
245 | 239, 244 | syl6bb 276 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))} ↔ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
246 | 238, 245 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → ((〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → 〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))}) ↔ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))))) |
247 | 236, 246 | syl5ibrcom 237 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → 〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))}))) |
248 | 247 | rexlimdvva 3186 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → 〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))}))) |
249 | 51, 248 | sylbird 250 |
. . . . . . . . 9
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (〈𝑥, 𝑦〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → 〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))}))) |
250 | 249 | com23 86 |
. . . . . . . 8
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → (〈𝑥, 𝑦〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) → 〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))}))) |
251 | 38, 250 | mpdd 43 |
. . . . . . 7
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → 〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))})) |
252 | 37, 251 | relssdv 5352 |
. . . . . 6
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (◡(-g‘𝐻) “ 𝑢) ⊆ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))}) |
253 | | ssabral 3822 |
. . . . . 6
⊢ ((◡(-g‘𝐻) “ 𝑢) ⊆ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))} ↔ ∀𝑤 ∈ (◡(-g‘𝐻) “ 𝑢)∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) |
254 | 252, 253 | sylib 208 |
. . . . 5
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → ∀𝑤 ∈ (◡(-g‘𝐻) “ 𝑢)∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) |
255 | | eltx 21592 |
. . . . . . 7
⊢ ((𝐾 ∈
(TopOn‘(Base‘𝐻)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → ((◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ (◡(-g‘𝐻) “ 𝑢)∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
256 | 23, 23, 255 | syl2anc 573 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ((◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ (◡(-g‘𝐻) “ 𝑢)∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
257 | 256 | adantr 466 |
. . . . 5
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → ((◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ (◡(-g‘𝐻) “ 𝑢)∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
258 | 254, 257 | mpbird 247 |
. . . 4
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾)) |
259 | 258 | ralrimiva 3115 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ∀𝑢 ∈ 𝐾 (◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾)) |
260 | | txtopon 21615 |
. . . . 5
⊢ ((𝐾 ∈
(TopOn‘(Base‘𝐻)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → (𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻)))) |
261 | 23, 23, 260 | syl2anc 573 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻)))) |
262 | | iscn 21260 |
. . . 4
⊢ (((𝐾 ×t 𝐾) ∈
(TopOn‘((Base‘𝐻) × (Base‘𝐻))) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) →
((-g‘𝐻)
∈ ((𝐾
×t 𝐾) Cn
𝐾) ↔
((-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) ∧ ∀𝑢 ∈ 𝐾 (◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾)))) |
263 | 261, 23, 262 | syl2anc 573 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
((-g‘𝐻)
∈ ((𝐾
×t 𝐾) Cn
𝐾) ↔
((-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) ∧ ∀𝑢 ∈ 𝐾 (◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾)))) |
264 | 29, 259, 263 | mpbir2and 692 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
(-g‘𝐻)
∈ ((𝐾
×t 𝐾) Cn
𝐾)) |
265 | 14, 27 | istgp2 22115 |
. 2
⊢ (𝐻 ∈ TopGrp ↔ (𝐻 ∈ Grp ∧ 𝐻 ∈ TopSp ∧
(-g‘𝐻)
∈ ((𝐾
×t 𝐾) Cn
𝐾))) |
266 | 3, 26, 264, 265 | syl3anbrc 1428 |
1
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopGrp) |