Step | Hyp | Ref
| Expression |
1 | | qustgp.h |
. . . 4
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌)) |
2 | 1 | qusgrp 17472 |
. . 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 6577 |
. . . . . . . 8
⊢ (𝐺 ~QG 𝑌) ∈ V |
9 | 8 | a1i 11 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐺 ~QG 𝑌) ∈ V) |
10 | | simpl 472 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐺 ∈ TopGrp) |
11 | 4, 6, 7, 9, 10 | qusval 16025 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 = (𝐹 “s 𝐺)) |
12 | 4, 6, 7, 9, 10 | quslem 16026 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹:𝑋–onto→(𝑋 / (𝐺 ~QG 𝑌))) |
13 | | qustgpopn.j |
. . . . . 6
⊢ 𝐽 = (TopOpen‘𝐺) |
14 | | qustgpopn.k |
. . . . . 6
⊢ 𝐾 = (TopOpen‘𝐻) |
15 | 11, 6, 12, 10, 13, 14 | imastopn 21333 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 = (𝐽 qTop 𝐹)) |
16 | 13, 5 | tgptopon 21696 |
. . . . . . 7
⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋)) |
17 | 16 | adantr 480 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐽 ∈ (TopOn‘𝑋)) |
18 | | qtoptopon 21317 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→(𝑋 / (𝐺 ~QG 𝑌))) → (𝐽 qTop 𝐹) ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌)))) |
19 | 17, 12, 18 | syl2anc 691 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐽 qTop 𝐹) ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌)))) |
20 | 15, 19 | eqeltrd 2688 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌)))) |
21 | 4, 6, 9, 10 | qusbas 16028 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑋 / (𝐺 ~QG 𝑌)) = (Base‘𝐻)) |
22 | 21 | fveq2d 6107 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))) = (TopOn‘(Base‘𝐻))) |
23 | 20, 22 | eleqtrd 2690 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 ∈ (TopOn‘(Base‘𝐻))) |
24 | | eqid 2610 |
. . . 4
⊢
(Base‘𝐻) =
(Base‘𝐻) |
25 | 24, 14 | istps 20551 |
. . 3
⊢ (𝐻 ∈ TopSp ↔ 𝐾 ∈
(TopOn‘(Base‘𝐻))) |
26 | 23, 25 | sylibr 223 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopSp) |
27 | | eqid 2610 |
. . . . 5
⊢
(-g‘𝐻) = (-g‘𝐻) |
28 | 24, 27 | grpsubf 17317 |
. . . 4
⊢ (𝐻 ∈ Grp →
(-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻)) |
29 | 3, 28 | syl 17 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
(-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻)) |
30 | | cnvimass 5404 |
. . . . . . . . 9
⊢ (◡(-g‘𝐻) “ 𝑢) ⊆ dom (-g‘𝐻) |
31 | | fdm 5964 |
. . . . . . . . . . 11
⊢
((-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) → dom (-g‘𝐻) = ((Base‘𝐻) × (Base‘𝐻))) |
32 | 29, 31 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → dom
(-g‘𝐻) =
((Base‘𝐻) ×
(Base‘𝐻))) |
33 | 32 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → dom (-g‘𝐻) = ((Base‘𝐻) × (Base‘𝐻))) |
34 | 30, 33 | syl5sseq 3616 |
. . . . . . . 8
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (◡(-g‘𝐻) “ 𝑢) ⊆ ((Base‘𝐻) × (Base‘𝐻))) |
35 | | relxp 5150 |
. . . . . . . 8
⊢ Rel
((Base‘𝐻) ×
(Base‘𝐻)) |
36 | | relss 5129 |
. . . . . . . 8
⊢ ((◡(-g‘𝐻) “ 𝑢) ⊆ ((Base‘𝐻) × (Base‘𝐻)) → (Rel ((Base‘𝐻) × (Base‘𝐻)) → Rel (◡(-g‘𝐻) “ 𝑢))) |
37 | 34, 35, 36 | mpisyl 21 |
. . . . . . 7
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → Rel (◡(-g‘𝐻) “ 𝑢)) |
38 | 34 | sseld 3567 |
. . . . . . . 8
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → 〈𝑥, 𝑦〉 ∈ ((Base‘𝐻) × (Base‘𝐻)))) |
39 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
40 | 39 | elqs 7686 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ ∃𝑎 ∈ 𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌)) |
41 | 21 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (𝑋 / (𝐺 ~QG 𝑌)) = (Base‘𝐻)) |
42 | 41 | eleq2d 2673 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (𝑥 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ 𝑥 ∈ (Base‘𝐻))) |
43 | 40, 42 | syl5bbr 273 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (∃𝑎 ∈ 𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ↔ 𝑥 ∈ (Base‘𝐻))) |
44 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V |
45 | 44 | elqs 7686 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ ∃𝑏 ∈ 𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌)) |
46 | 41 | eleq2d 2673 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (𝑦 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ 𝑦 ∈ (Base‘𝐻))) |
47 | 45, 46 | syl5bbr 273 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (∃𝑏 ∈ 𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌) ↔ 𝑦 ∈ (Base‘𝐻))) |
48 | 43, 47 | anbi12d 743 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → ((∃𝑎 ∈ 𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ ∃𝑏 ∈ 𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻)))) |
49 | | reeanv 3086 |
. . . . . . . . . . 11
⊢
(∃𝑎 ∈
𝑋 ∃𝑏 ∈ 𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ (∃𝑎 ∈ 𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ ∃𝑏 ∈ 𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌))) |
50 | | opelxp 5070 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) |
51 | 48, 49, 50 | 3bitr4g 302 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ 〈𝑥, 𝑦〉 ∈ ((Base‘𝐻) × (Base‘𝐻)))) |
52 | 3 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝐻 ∈ Grp) |
53 | 52, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻)) |
54 | | ffn 5958 |
. . . . . . . . . . . . . 14
⊢
((-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) → (-g‘𝐻) Fn ((Base‘𝐻) × (Base‘𝐻))) |
55 | | elpreima 6245 |
. . . . . . . . . . . . . 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 6552 |
. . . . . . . . . . . . . . . . 17
⊢ ([𝑎](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑏](𝐺 ~QG 𝑌)) = ((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) |
58 | | simpllr 795 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑌 ∈ (NrmSGrp‘𝐺)) |
59 | | simprl 790 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑎 ∈ 𝑋) |
60 | | simprr 792 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑏 ∈ 𝑋) |
61 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢
(-g‘𝐺) = (-g‘𝐺) |
62 | 1, 5, 61, 27 | qussub 17477 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ([𝑎](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑏](𝐺 ~QG 𝑌)) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) |
63 | 58, 59, 60, 62 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ([𝑎](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑏](𝐺 ~QG 𝑌)) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) |
64 | 57, 63 | syl5eqr 2658 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) |
65 | 64 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) ∈ 𝑢 ↔ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢)) |
66 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) |
67 | | qustgplem.m |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ − =
(𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌)) |
68 | | tgpgrp 21692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
69 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐺 ∈ Grp) |
70 | 5, 61 | grpsubf 17317 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐺 ∈ Grp →
(-g‘𝐺):(𝑋 × 𝑋)⟶𝑋) |
71 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((-g‘𝐺):(𝑋 × 𝑋)⟶𝑋 → (-g‘𝐺) Fn (𝑋 × 𝑋)) |
72 | 69, 70, 71 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
(-g‘𝐺) Fn
(𝑋 × 𝑋)) |
73 | | fnov 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((-g‘𝐺) Fn (𝑋 × 𝑋) ↔ (-g‘𝐺) = (𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ (𝑧(-g‘𝐺)𝑤))) |
74 | 72, 73 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
(-g‘𝐺) =
(𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ (𝑧(-g‘𝐺)𝑤))) |
75 | 13, 61 | tgpsubcn 21704 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐺 ∈ TopGrp →
(-g‘𝐺)
∈ ((𝐽
×t 𝐽) Cn
𝐽)) |
76 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
(-g‘𝐺)
∈ ((𝐽
×t 𝐽) Cn
𝐽)) |
77 | 74, 76 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ (𝑧(-g‘𝐺)𝑤)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
78 | | ecexg 7633 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐺 ~QG 𝑌) ∈ V → [𝑥](𝐺 ~QG 𝑌) ∈ V) |
79 | 8, 78 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ [𝑥](𝐺 ~QG 𝑌) ∈ V |
80 | 79, 7 | fnmpti 5935 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝐹 Fn 𝑋 |
81 | | qtopid 21318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 Fn 𝑋) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))) |
82 | 17, 80, 81 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))) |
83 | 15 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐽 Cn 𝐾) = (𝐽 Cn (𝐽 qTop 𝐹))) |
84 | 82, 83 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
85 | 7, 84 | syl5eqelr 2693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑥 ∈ 𝑋 ↦ [𝑥](𝐺 ~QG 𝑌)) ∈ (𝐽 Cn 𝐾)) |
86 | | eceq1 7669 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = (𝑧(-g‘𝐺)𝑤) → [𝑥](𝐺 ~QG 𝑌) = [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌)) |
87 | 17, 17, 77, 17, 85, 86 | cnmpt21 21284 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌)) ∈ ((𝐽 ×t 𝐽) Cn 𝐾)) |
88 | 67, 87 | syl5eqel 2692 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → − ∈ ((𝐽 ×t 𝐽) Cn 𝐾)) |
89 | 88 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → − ∈ ((𝐽 ×t 𝐽) Cn 𝐾)) |
90 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑢 ∈ 𝐾) |
91 | | cnima 20879 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (( − ∈
((𝐽 ×t
𝐽) Cn 𝐾) ∧ 𝑢 ∈ 𝐾) → (◡ − “ 𝑢) ∈ (𝐽 ×t 𝐽)) |
92 | 89, 90, 91 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (◡ − “ 𝑢) ∈ (𝐽 ×t 𝐽)) |
93 | 17 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝐽 ∈ (TopOn‘𝑋)) |
94 | | eltx 21181 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘𝑋)) → ((◡ − “ 𝑢) ∈ (𝐽 ×t 𝐽) ↔ ∀𝑡 ∈ (◡ − “ 𝑢)∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) |
95 | 93, 93, 94 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((◡ − “ 𝑢) ∈ (𝐽 ×t 𝐽) ↔ ∀𝑡 ∈ (◡ − “ 𝑢)∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) |
96 | 92, 95 | mpbid 221 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ∀𝑡 ∈ (◡ − “ 𝑢)∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢))) |
97 | | ecexg 7633 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ~QG 𝑌) ∈ V → [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌) ∈ V) |
98 | 8, 97 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌) ∈ V |
99 | 67, 98 | fnmpt2i 7128 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ − Fn
(𝑋 × 𝑋) |
100 | | elpreima 6245 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ( − Fn
(𝑋 × 𝑋) → (〈𝑎, 𝑏〉 ∈ (◡ − “ 𝑢) ↔ (〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋) ∧ ( − ‘〈𝑎, 𝑏〉) ∈ 𝑢))) |
101 | 99, 100 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑎, 𝑏〉 ∈ (◡ − “ 𝑢) ↔ (〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋) ∧ ( − ‘〈𝑎, 𝑏〉) ∈ 𝑢)) |
102 | | opelxp 5070 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋) ↔ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) |
103 | 102 | anbi1i 727 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋) ∧ ( − ‘〈𝑎, 𝑏〉) ∈ 𝑢) ↔ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ ( − ‘〈𝑎, 𝑏〉) ∈ 𝑢)) |
104 | | df-ov 6552 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 − 𝑏) = ( − ‘〈𝑎, 𝑏〉) |
105 | | oveq12 6558 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 = 𝑎 ∧ 𝑤 = 𝑏) → (𝑧(-g‘𝐺)𝑤) = (𝑎(-g‘𝐺)𝑏)) |
106 | 105 | eceq1d 7670 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 = 𝑎 ∧ 𝑤 = 𝑏) → [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) |
107 | | ecexg 7633 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ~QG 𝑌) ∈ V → [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ V) |
108 | 8, 107 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ V |
109 | 106, 67, 108 | ovmpt2a 6689 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑎 − 𝑏) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) |
110 | 104, 109 | syl5eqr 2658 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ( − ‘〈𝑎, 𝑏〉) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) |
111 | 110 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (( − ‘〈𝑎, 𝑏〉) ∈ 𝑢 ↔ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢)) |
112 | 111 | pm5.32i 667 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ ( − ‘〈𝑎, 𝑏〉) ∈ 𝑢) ↔ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢)) |
113 | 101, 103,
112 | 3bitri 285 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑎, 𝑏〉 ∈ (◡ − “ 𝑢) ↔ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢)) |
114 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 〈𝑎, 𝑏〉 → (𝑡 ∈ (𝑐 × 𝑑) ↔ 〈𝑎, 𝑏〉 ∈ (𝑐 × 𝑑))) |
115 | | opelxp 5070 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈𝑎, 𝑏〉 ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑)) |
116 | 114, 115 | syl6bb 275 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 〈𝑎, 𝑏〉 → (𝑡 ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑))) |
117 | 116 | anbi1d 737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 〈𝑎, 𝑏〉 → ((𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) |
118 | 117 | 2rexbidv 3039 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 〈𝑎, 𝑏〉 → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) ↔ ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) |
119 | 118 | rspccv 3279 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑡 ∈
(◡ − “ 𝑢)∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) → (〈𝑎, 𝑏〉 ∈ (◡ − “ 𝑢) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) |
120 | 113, 119 | syl5bir 232 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑡 ∈
(◡ − “ 𝑢)∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) → (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) |
121 | 96, 120 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) |
122 | 66, 121 | mpand 707 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ([(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) |
123 | | simp-4l 802 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝐺 ∈ TopGrp) |
124 | 58 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑌 ∈ (NrmSGrp‘𝐺)) |
125 | | simprll 798 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑐 ∈ 𝐽) |
126 | 1, 5, 13, 14, 7 | qustgpopn 21733 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑐 ∈ 𝐽) → (𝐹 “ 𝑐) ∈ 𝐾) |
127 | 123, 124,
125, 126 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹 “ 𝑐) ∈ 𝐾) |
128 | | simprlr 799 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑑 ∈ 𝐽) |
129 | 1, 5, 13, 14, 7 | qustgpopn 21733 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑑 ∈ 𝐽) → (𝐹 “ 𝑑) ∈ 𝐾) |
130 | 123, 124,
128, 129 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹 “ 𝑑) ∈ 𝐾) |
131 | 59 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑎 ∈ 𝑋) |
132 | | eceq1 7669 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑎 → [𝑥](𝐺 ~QG 𝑌) = [𝑎](𝐺 ~QG 𝑌)) |
133 | 132, 7, 79 | fvmpt3i 6196 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 ∈ 𝑋 → (𝐹‘𝑎) = [𝑎](𝐺 ~QG 𝑌)) |
134 | 131, 133 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹‘𝑎) = [𝑎](𝐺 ~QG 𝑌)) |
135 | 123, 16 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝐽 ∈ (TopOn‘𝑋)) |
136 | | toponss 20544 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑐 ∈ 𝐽) → 𝑐 ⊆ 𝑋) |
137 | 135, 125,
136 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑐 ⊆ 𝑋) |
138 | | simprrl 800 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑)) |
139 | 138 | simpld 474 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑎 ∈ 𝑐) |
140 | | fnfvima 6400 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹 Fn 𝑋 ∧ 𝑐 ⊆ 𝑋 ∧ 𝑎 ∈ 𝑐) → (𝐹‘𝑎) ∈ (𝐹 “ 𝑐)) |
141 | 80, 140 | mp3an1 1403 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑐 ⊆ 𝑋 ∧ 𝑎 ∈ 𝑐) → (𝐹‘𝑎) ∈ (𝐹 “ 𝑐)) |
142 | 137, 139,
141 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹‘𝑎) ∈ (𝐹 “ 𝑐)) |
143 | 134, 142 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → [𝑎](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑐)) |
144 | 60 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑏 ∈ 𝑋) |
145 | | eceq1 7669 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑏 → [𝑥](𝐺 ~QG 𝑌) = [𝑏](𝐺 ~QG 𝑌)) |
146 | 145, 7, 79 | fvmpt3i 6196 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 ∈ 𝑋 → (𝐹‘𝑏) = [𝑏](𝐺 ~QG 𝑌)) |
147 | 144, 146 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹‘𝑏) = [𝑏](𝐺 ~QG 𝑌)) |
148 | | toponss 20544 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑑 ∈ 𝐽) → 𝑑 ⊆ 𝑋) |
149 | 135, 128,
148 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑑 ⊆ 𝑋) |
150 | 138 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑏 ∈ 𝑑) |
151 | | fnfvima 6400 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹 Fn 𝑋 ∧ 𝑑 ⊆ 𝑋 ∧ 𝑏 ∈ 𝑑) → (𝐹‘𝑏) ∈ (𝐹 “ 𝑑)) |
152 | 80, 151 | mp3an1 1403 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑑 ⊆ 𝑋 ∧ 𝑏 ∈ 𝑑) → (𝐹‘𝑏) ∈ (𝐹 “ 𝑑)) |
153 | 149, 150,
152 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹‘𝑏) ∈ (𝐹 “ 𝑑)) |
154 | 147, 153 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → [𝑏](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑑)) |
155 | | opelxpi 5072 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (([𝑎](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑐) ∧ [𝑏](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑑)) → 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑))) |
156 | 143, 154,
155 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑))) |
157 | 137 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ 𝑝 ∈ 𝑐) → 𝑝 ∈ 𝑋) |
158 | 149 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ 𝑞 ∈ 𝑑) → 𝑞 ∈ 𝑋) |
159 | 157, 158 | anim12dan 878 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) |
160 | | eceq1 7669 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 𝑝 → [𝑥](𝐺 ~QG 𝑌) = [𝑝](𝐺 ~QG 𝑌)) |
161 | 160, 7, 79 | fvmpt3i 6196 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑝 ∈ 𝑋 → (𝐹‘𝑝) = [𝑝](𝐺 ~QG 𝑌)) |
162 | | eceq1 7669 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 𝑞 → [𝑥](𝐺 ~QG 𝑌) = [𝑞](𝐺 ~QG 𝑌)) |
163 | 162, 7, 79 | fvmpt3i 6196 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑞 ∈ 𝑋 → (𝐹‘𝑞) = [𝑞](𝐺 ~QG 𝑌)) |
164 | | opeq12 4342 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐹‘𝑝) = [𝑝](𝐺 ~QG 𝑌) ∧ (𝐹‘𝑞) = [𝑞](𝐺 ~QG 𝑌)) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 = 〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) |
165 | 161, 163,
164 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 = 〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) |
166 | 159, 165 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 = 〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) |
167 | 124 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → 𝑌 ∈ (NrmSGrp‘𝐺)) |
168 | 1, 5, 24 | quseccl 17473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑝 ∈ 𝑋) → [𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)) |
169 | 1, 5, 24 | quseccl 17473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑞 ∈ 𝑋) → [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)) |
170 | 168, 169 | anim12dan 878 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻))) |
171 | 167, 159,
170 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻))) |
172 | | opelxpi 5072 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 17477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → ([𝑝](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) |
175 | 174 | 3expb 1258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ([𝑝](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) |
176 | 167, 159,
175 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ([𝑝](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) |
177 | | oveq12 6558 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑧 = 𝑝 ∧ 𝑤 = 𝑞) → (𝑧(-g‘𝐺)𝑤) = (𝑝(-g‘𝐺)𝑞)) |
178 | 177 | eceq1d 7670 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑧 = 𝑝 ∧ 𝑤 = 𝑞) → [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) |
179 | | ecexg 7633 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐺 ~QG 𝑌) ∈ V → [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌) ∈ V) |
180 | 8, 179 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌) ∈ V |
181 | 178, 67, 180 | ovmpt2a 6689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → (𝑝 − 𝑞) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) |
182 | 159, 181 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → (𝑝 − 𝑞) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) |
183 | 176, 182 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ([𝑝](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑞](𝐺 ~QG 𝑌)) = (𝑝 − 𝑞)) |
184 | | df-ov 6552 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ([𝑝](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑞](𝐺 ~QG 𝑌)) = ((-g‘𝐻)‘〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) |
185 | | df-ov 6552 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑝 − 𝑞) = ( − ‘〈𝑝, 𝑞〉) |
186 | 183, 184,
185 | 3eqtr3g 2667 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ((-g‘𝐻)‘〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) = ( − ‘〈𝑝, 𝑞〉)) |
187 | | opelxpi 5072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑) → 〈𝑝, 𝑞〉 ∈ (𝑐 × 𝑑)) |
188 | | simprrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) |
189 | 188 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ 〈𝑝, 𝑞〉 ∈ (𝑐 × 𝑑)) → 〈𝑝, 𝑞〉 ∈ (◡ − “ 𝑢)) |
190 | 187, 189 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → 〈𝑝, 𝑞〉 ∈ (◡ − “ 𝑢)) |
191 | | elpreima 6245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ( − Fn
(𝑋 × 𝑋) → (〈𝑝, 𝑞〉 ∈ (◡ − “ 𝑢) ↔ (〈𝑝, 𝑞〉 ∈ (𝑋 × 𝑋) ∧ ( − ‘〈𝑝, 𝑞〉) ∈ 𝑢))) |
192 | 99, 191 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(〈𝑝, 𝑞〉 ∈ (◡ − “ 𝑢) ↔ (〈𝑝, 𝑞〉 ∈ (𝑋 × 𝑋) ∧ ( − ‘〈𝑝, 𝑞〉) ∈ 𝑢)) |
193 | 192 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(〈𝑝, 𝑞〉 ∈ (◡ − “ 𝑢) → ( − ‘〈𝑝, 𝑞〉) ∈ 𝑢) |
194 | 190, 193 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ( − ‘〈𝑝, 𝑞〉) ∈ 𝑢) |
195 | 186, 194 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ((-g‘𝐻)‘〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) ∈ 𝑢) |
196 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (-g‘𝐻) Fn ((Base‘𝐻) × (Base‘𝐻))) |
197 | 196 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → (-g‘𝐻) Fn ((Base‘𝐻) × (Base‘𝐻))) |
198 | | elpreima 6245 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 959 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → 〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢)) |
201 | 166, 200 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢)) |
202 | 201 | ralrimivva 2954 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → ∀𝑝 ∈ 𝑐 ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢)) |
203 | | opeq1 4340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 = (𝐹‘𝑝) → 〈𝑧, 𝑤〉 = 〈(𝐹‘𝑝), 𝑤〉) |
204 | 203 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 = (𝐹‘𝑝) → (〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ 〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
205 | 204 | ralbidv 2969 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = (𝐹‘𝑝) → (∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
206 | 205 | ralima 6402 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹 Fn 𝑋 ∧ 𝑐 ⊆ 𝑋) → (∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑝 ∈ 𝑐 ∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
207 | 80, 206 | mpan 702 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 ⊆ 𝑋 → (∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑝 ∈ 𝑐 ∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
208 | | opeq2 4341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 = (𝐹‘𝑞) → 〈(𝐹‘𝑝), 𝑤〉 = 〈(𝐹‘𝑝), (𝐹‘𝑞)〉) |
209 | 208 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 = (𝐹‘𝑞) → (〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
210 | 209 | ralima 6402 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹 Fn 𝑋 ∧ 𝑑 ⊆ 𝑋) → (∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
211 | 80, 210 | mpan 702 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑑 ⊆ 𝑋 → (∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
212 | 211 | ralbidv 2969 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑑 ⊆ 𝑋 → (∀𝑝 ∈ 𝑐 ∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑝 ∈ 𝑐 ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
213 | 207, 212 | sylan9bb 732 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑐 ⊆ 𝑋 ∧ 𝑑 ⊆ 𝑋) → (∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑝 ∈ 𝑐 ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
214 | 137, 149,
213 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑝 ∈ 𝑐 ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
215 | 202, 214 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → ∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢)) |
216 | | dfss3 3558 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑦 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑))𝑦 ∈ (◡(-g‘𝐻) “ 𝑢)) |
217 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 〈𝑧, 𝑤〉 → (𝑦 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ 〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
218 | 217 | ralxp 5185 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑦 ∈
((𝐹 “ 𝑐) × (𝐹 “ 𝑑))𝑦 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢)) |
219 | 216, 218 | bitri 263 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢)) |
220 | 215, 219 | sylibr 223 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢)) |
221 | | xpeq1 5052 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑟 = (𝐹 “ 𝑐) → (𝑟 × 𝑠) = ((𝐹 “ 𝑐) × 𝑠)) |
222 | 221 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 = (𝐹 “ 𝑐) → (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ↔ 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × 𝑠))) |
223 | 221 | sseq1d 3595 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 = (𝐹 “ 𝑐) → ((𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢) ↔ ((𝐹 “ 𝑐) × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) |
224 | 222, 223 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 = (𝐹 “ 𝑐) → ((〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)) ↔ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × 𝑠) ∧ ((𝐹 “ 𝑐) × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
225 | | xpeq2 5053 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 = (𝐹 “ 𝑑) → ((𝐹 “ 𝑐) × 𝑠) = ((𝐹 “ 𝑐) × (𝐹 “ 𝑑))) |
226 | 225 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = (𝐹 “ 𝑑) → (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × 𝑠) ↔ 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)))) |
227 | 225 | sseq1d 3595 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = (𝐹 “ 𝑑) → (((𝐹 “ 𝑐) × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢) ↔ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢))) |
228 | 226, 227 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = (𝐹 “ 𝑑) → ((〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × 𝑠) ∧ ((𝐹 “ 𝑐) × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)) ↔ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ∧ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
229 | 224, 228 | rspc2ev 3295 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹 “ 𝑐) ∈ 𝐾 ∧ (𝐹 “ 𝑑) ∈ 𝐾 ∧ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ∧ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢))) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) |
230 | 127, 130,
156, 220, 229 | syl112anc 1322 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) |
231 | 230 | expr 641 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
232 | 231 | rexlimdvva 3020 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
233 | 122, 232 | syld 46 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ([(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢 → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
234 | 65, 233 | sylbid 229 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) ∈ 𝑢 → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
235 | 234 | adantld 482 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧
((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) ∈ 𝑢) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
236 | 56, 235 | sylbid 229 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
237 | | opeq12 4342 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → 〈𝑥, 𝑦〉 = 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) |
238 | 237 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
239 | 237 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))} ↔ 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))})) |
240 | | opex 4859 |
. . . . . . . . . . . . . . 15
⊢
〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ V |
241 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 → (𝑤 ∈ (𝑟 × 𝑠) ↔ 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠))) |
242 | 241 | anbi1d 737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 → ((𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)) ↔ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
243 | 242 | 2rexbidv 3039 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 → (∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)) ↔ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
244 | 240, 243 | elab 3319 |
. . . . . . . . . . . . . 14
⊢
(〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))} ↔ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) |
245 | 239, 244 | syl6bb 275 |
. . . . . . . . . . . . 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 236 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → 〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))}))) |
248 | 247 | rexlimdvva 3020 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → 〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))}))) |
249 | 51, 248 | sylbird 249 |
. . . . . . . . 9
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (〈𝑥, 𝑦〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → 〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))}))) |
250 | 249 | com23 84 |
. . . . . . . 8
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → (〈𝑥, 𝑦〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) → 〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))}))) |
251 | 38, 250 | mpdd 42 |
. . . . . . 7
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → 〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))})) |
252 | 37, 251 | relssdv 5135 |
. . . . . 6
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (◡(-g‘𝐻) “ 𝑢) ⊆ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))}) |
253 | | ssabral 3636 |
. . . . . 6
⊢ ((◡(-g‘𝐻) “ 𝑢) ⊆ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))} ↔ ∀𝑤 ∈ (◡(-g‘𝐻) “ 𝑢)∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) |
254 | 252, 253 | sylib 207 |
. . . . 5
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → ∀𝑤 ∈ (◡(-g‘𝐻) “ 𝑢)∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) |
255 | | eltx 21181 |
. . . . . . 7
⊢ ((𝐾 ∈
(TopOn‘(Base‘𝐻)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → ((◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ (◡(-g‘𝐻) “ 𝑢)∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
256 | 23, 23, 255 | syl2anc 691 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ((◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ (◡(-g‘𝐻) “ 𝑢)∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
257 | 256 | adantr 480 |
. . . . 5
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → ((◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ (◡(-g‘𝐻) “ 𝑢)∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
258 | 254, 257 | mpbird 246 |
. . . 4
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾)) |
259 | 258 | ralrimiva 2949 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ∀𝑢 ∈ 𝐾 (◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾)) |
260 | | txtopon 21204 |
. . . . 5
⊢ ((𝐾 ∈
(TopOn‘(Base‘𝐻)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → (𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻)))) |
261 | 23, 23, 260 | syl2anc 691 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻)))) |
262 | | iscn 20849 |
. . . 4
⊢ (((𝐾 ×t 𝐾) ∈
(TopOn‘((Base‘𝐻) × (Base‘𝐻))) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) →
((-g‘𝐻)
∈ ((𝐾
×t 𝐾) Cn
𝐾) ↔
((-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) ∧ ∀𝑢 ∈ 𝐾 (◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾)))) |
263 | 261, 23, 262 | syl2anc 691 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
((-g‘𝐻)
∈ ((𝐾
×t 𝐾) Cn
𝐾) ↔
((-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) ∧ ∀𝑢 ∈ 𝐾 (◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾)))) |
264 | 29, 259, 263 | mpbir2and 959 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
(-g‘𝐻)
∈ ((𝐾
×t 𝐾) Cn
𝐾)) |
265 | 14, 27 | istgp2 21705 |
. 2
⊢ (𝐻 ∈ TopGrp ↔ (𝐻 ∈ Grp ∧ 𝐻 ∈ TopSp ∧
(-g‘𝐻)
∈ ((𝐾
×t 𝐾) Cn
𝐾))) |
266 | 3, 26, 264, 265 | syl3anbrc 1239 |
1
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopGrp) |