Step | Hyp | Ref
| Expression |
1 | | qustgp.h |
. . . 4
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌)) |
2 | 1 | qusgrp 18453 |
. . 3
⊢ (𝑌 ∈ (NrmSGrp‘𝐺) → 𝐻 ∈ Grp) |
3 | 2 | adantl 485 |
. 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 7203 |
. . . . . . . 8
⊢ (𝐺 ~QG 𝑌) ∈ V |
9 | 8 | a1i 11 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐺 ~QG 𝑌) ∈ V) |
10 | | simpl 486 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐺 ∈ TopGrp) |
11 | 4, 6, 7, 9, 10 | qusval 16918 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 = (𝐹 “s 𝐺)) |
12 | 4, 6, 7, 9, 10 | quslem 16919 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹:𝑋–onto→(𝑋 / (𝐺 ~QG 𝑌))) |
13 | | qustgpopn.j |
. . . . . 6
⊢ 𝐽 = (TopOpen‘𝐺) |
14 | | qustgpopn.k |
. . . . . 6
⊢ 𝐾 = (TopOpen‘𝐻) |
15 | 11, 6, 12, 10, 13, 14 | imastopn 22471 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 = (𝐽 qTop 𝐹)) |
16 | 13, 5 | tgptopon 22833 |
. . . . . . 7
⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋)) |
17 | 16 | adantr 484 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐽 ∈ (TopOn‘𝑋)) |
18 | | qtoptopon 22455 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→(𝑋 / (𝐺 ~QG 𝑌))) → (𝐽 qTop 𝐹) ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌)))) |
19 | 17, 12, 18 | syl2anc 587 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐽 qTop 𝐹) ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌)))) |
20 | 15, 19 | eqeltrd 2833 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 ∈ (TopOn‘(𝑋 / (𝐺 ~QG 𝑌)))) |
21 | 4, 6, 9, 10 | qusbas 16921 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑋 / (𝐺 ~QG 𝑌)) = (Base‘𝐻)) |
22 | 21 | fveq2d 6678 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (TopOn‘(𝑋 / (𝐺 ~QG 𝑌))) = (TopOn‘(Base‘𝐻))) |
23 | 20, 22 | eleqtrd 2835 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐾 ∈ (TopOn‘(Base‘𝐻))) |
24 | | eqid 2738 |
. . . 4
⊢
(Base‘𝐻) =
(Base‘𝐻) |
25 | 24, 14 | istps 21685 |
. . 3
⊢ (𝐻 ∈ TopSp ↔ 𝐾 ∈
(TopOn‘(Base‘𝐻))) |
26 | 23, 25 | sylibr 237 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopSp) |
27 | | eqid 2738 |
. . . . 5
⊢
(-g‘𝐻) = (-g‘𝐻) |
28 | 24, 27 | grpsubf 18296 |
. . . 4
⊢ (𝐻 ∈ Grp →
(-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻)) |
29 | 3, 28 | syl 17 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
(-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻)) |
30 | | cnvimass 5923 |
. . . . . . . . 9
⊢ (◡(-g‘𝐻) “ 𝑢) ⊆ dom (-g‘𝐻) |
31 | 29 | fdmd 6515 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → dom
(-g‘𝐻) =
((Base‘𝐻) ×
(Base‘𝐻))) |
32 | 31 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → dom (-g‘𝐻) = ((Base‘𝐻) × (Base‘𝐻))) |
33 | 30, 32 | sseqtrid 3929 |
. . . . . . . 8
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (◡(-g‘𝐻) “ 𝑢) ⊆ ((Base‘𝐻) × (Base‘𝐻))) |
34 | | relxp 5543 |
. . . . . . . 8
⊢ Rel
((Base‘𝐻) ×
(Base‘𝐻)) |
35 | | relss 5627 |
. . . . . . . 8
⊢ ((◡(-g‘𝐻) “ 𝑢) ⊆ ((Base‘𝐻) × (Base‘𝐻)) → (Rel ((Base‘𝐻) × (Base‘𝐻)) → Rel (◡(-g‘𝐻) “ 𝑢))) |
36 | 33, 34, 35 | mpisyl 21 |
. . . . . . 7
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → Rel (◡(-g‘𝐻) “ 𝑢)) |
37 | 33 | sseld 3876 |
. . . . . . . 8
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → 〈𝑥, 𝑦〉 ∈ ((Base‘𝐻) × (Base‘𝐻)))) |
38 | | vex 3402 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
39 | 38 | elqs 8380 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ ∃𝑎 ∈ 𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌)) |
40 | 21 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (𝑋 / (𝐺 ~QG 𝑌)) = (Base‘𝐻)) |
41 | 40 | eleq2d 2818 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (𝑥 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ 𝑥 ∈ (Base‘𝐻))) |
42 | 39, 41 | bitr3id 288 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (∃𝑎 ∈ 𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ↔ 𝑥 ∈ (Base‘𝐻))) |
43 | | vex 3402 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V |
44 | 43 | elqs 8380 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ ∃𝑏 ∈ 𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌)) |
45 | 40 | eleq2d 2818 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (𝑦 ∈ (𝑋 / (𝐺 ~QG 𝑌)) ↔ 𝑦 ∈ (Base‘𝐻))) |
46 | 44, 45 | bitr3id 288 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (∃𝑏 ∈ 𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌) ↔ 𝑦 ∈ (Base‘𝐻))) |
47 | 42, 46 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → ((∃𝑎 ∈ 𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ ∃𝑏 ∈ 𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻)))) |
48 | | reeanv 3270 |
. . . . . . . . . . 11
⊢
(∃𝑎 ∈
𝑋 ∃𝑏 ∈ 𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) ↔ (∃𝑎 ∈ 𝑋 𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ ∃𝑏 ∈ 𝑋 𝑦 = [𝑏](𝐺 ~QG 𝑌))) |
49 | | opelxp 5561 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) ↔ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) |
50 | 47, 48, 49 | 3bitr4g 317 |
. . . . . . . . . 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 6504 |
. . . . . . . . . . . . . 14
⊢
((-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) → (-g‘𝐻) Fn ((Base‘𝐻) × (Base‘𝐻))) |
54 | | elpreima 6835 |
. . . . . . . . . . . . . 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 7173 |
. . . . . . . . . . . . . . . . 17
⊢ ([𝑎](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑏](𝐺 ~QG 𝑌)) = ((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) |
57 | | simpllr 776 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑌 ∈ (NrmSGrp‘𝐺)) |
58 | | simprl 771 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑎 ∈ 𝑋) |
59 | | simprr 773 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑏 ∈ 𝑋) |
60 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . 19
⊢
(-g‘𝐺) = (-g‘𝐺) |
61 | 1, 5, 60, 27 | qussub 18458 |
. . . . . . . . . . . . . . . . . 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 2787 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) |
64 | 63 | eleq1d 2817 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) ∈ 𝑢 ↔ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢)) |
65 | | simpr 488 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) |
66 | | qustgplem.m |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ − =
(𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌)) |
67 | | tgpgrp 22829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
68 | 67 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐺 ∈ Grp) |
69 | 5, 60 | grpsubf 18296 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐺 ∈ Grp →
(-g‘𝐺):(𝑋 × 𝑋)⟶𝑋) |
70 | | ffn 6504 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((-g‘𝐺):(𝑋 × 𝑋)⟶𝑋 → (-g‘𝐺) Fn (𝑋 × 𝑋)) |
71 | 68, 69, 70 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
(-g‘𝐺) Fn
(𝑋 × 𝑋)) |
72 | | fnov 7297 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((-g‘𝐺) Fn (𝑋 × 𝑋) ↔ (-g‘𝐺) = (𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ (𝑧(-g‘𝐺)𝑤))) |
73 | 71, 72 | sylib 221 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
(-g‘𝐺) =
(𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ (𝑧(-g‘𝐺)𝑤))) |
74 | 13, 60 | tgpsubcn 22841 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐺 ∈ TopGrp →
(-g‘𝐺)
∈ ((𝐽
×t 𝐽) Cn
𝐽)) |
75 | 74 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) →
(-g‘𝐺)
∈ ((𝐽
×t 𝐽) Cn
𝐽)) |
76 | 73, 75 | eqeltrrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ (𝑧(-g‘𝐺)𝑤)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
77 | | ecexg 8324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐺 ~QG 𝑌) ∈ V → [𝑥](𝐺 ~QG 𝑌) ∈ V) |
78 | 8, 77 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ [𝑥](𝐺 ~QG 𝑌) ∈ V |
79 | 78, 7 | fnmpti 6480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝐹 Fn 𝑋 |
80 | | qtopid 22456 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 Fn 𝑋) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))) |
81 | 17, 79, 80 | sylancl 589 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))) |
82 | 15 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐽 Cn 𝐾) = (𝐽 Cn (𝐽 qTop 𝐹))) |
83 | 81, 82 | eleqtrrd 2836 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
84 | 7, 83 | eqeltrrid 2838 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑥 ∈ 𝑋 ↦ [𝑥](𝐺 ~QG 𝑌)) ∈ (𝐽 Cn 𝐾)) |
85 | | eceq1 8358 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = (𝑧(-g‘𝐺)𝑤) → [𝑥](𝐺 ~QG 𝑌) = [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌)) |
86 | 17, 17, 76, 17, 84, 85 | cnmpt21 22422 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌)) ∈ ((𝐽 ×t 𝐽) Cn 𝐾)) |
87 | 66, 86 | eqeltrid 2837 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → − ∈ ((𝐽 ×t 𝐽) Cn 𝐾)) |
88 | 87 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → − ∈ ((𝐽 ×t 𝐽) Cn 𝐾)) |
89 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑢 ∈ 𝐾) |
90 | | cnima 22016 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (( − ∈
((𝐽 ×t
𝐽) Cn 𝐾) ∧ 𝑢 ∈ 𝐾) → (◡ − “ 𝑢) ∈ (𝐽 ×t 𝐽)) |
91 | 88, 89, 90 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (◡ − “ 𝑢) ∈ (𝐽 ×t 𝐽)) |
92 | 17 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝐽 ∈ (TopOn‘𝑋)) |
93 | | eltx 22319 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘𝑋)) → ((◡ − “ 𝑢) ∈ (𝐽 ×t 𝐽) ↔ ∀𝑡 ∈ (◡ − “ 𝑢)∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) |
94 | 92, 92, 93 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((◡ − “ 𝑢) ∈ (𝐽 ×t 𝐽) ↔ ∀𝑡 ∈ (◡ − “ 𝑢)∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) |
95 | 91, 94 | mpbid 235 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ∀𝑡 ∈ (◡ − “ 𝑢)∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢))) |
96 | | ecexg 8324 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ~QG 𝑌) ∈ V → [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌) ∈ V) |
97 | 8, 96 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌) ∈ V |
98 | 66, 97 | fnmpoi 7793 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ − Fn
(𝑋 × 𝑋) |
99 | | elpreima 6835 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ( − Fn
(𝑋 × 𝑋) → (〈𝑎, 𝑏〉 ∈ (◡ − “ 𝑢) ↔ (〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋) ∧ ( − ‘〈𝑎, 𝑏〉) ∈ 𝑢))) |
100 | 98, 99 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑎, 𝑏〉 ∈ (◡ − “ 𝑢) ↔ (〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋) ∧ ( − ‘〈𝑎, 𝑏〉) ∈ 𝑢)) |
101 | | opelxp 5561 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋) ↔ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) |
102 | 101 | anbi1i 627 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋) ∧ ( − ‘〈𝑎, 𝑏〉) ∈ 𝑢) ↔ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ ( − ‘〈𝑎, 𝑏〉) ∈ 𝑢)) |
103 | | df-ov 7173 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 − 𝑏) = ( − ‘〈𝑎, 𝑏〉) |
104 | | oveq12 7179 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 = 𝑎 ∧ 𝑤 = 𝑏) → (𝑧(-g‘𝐺)𝑤) = (𝑎(-g‘𝐺)𝑏)) |
105 | 104 | eceq1d 8359 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 = 𝑎 ∧ 𝑤 = 𝑏) → [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) |
106 | | ecexg 8324 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ~QG 𝑌) ∈ V → [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ V) |
107 | 8, 106 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ V |
108 | 105, 66, 107 | ovmpoa 7320 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑎 − 𝑏) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) |
109 | 103, 108 | eqtr3id 2787 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ( − ‘〈𝑎, 𝑏〉) = [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌)) |
110 | 109 | eleq1d 2817 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (( − ‘〈𝑎, 𝑏〉) ∈ 𝑢 ↔ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢)) |
111 | 110 | pm5.32i 578 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ ( − ‘〈𝑎, 𝑏〉) ∈ 𝑢) ↔ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢)) |
112 | 100, 102,
111 | 3bitri 300 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑎, 𝑏〉 ∈ (◡ − “ 𝑢) ↔ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ [(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢)) |
113 | | eleq1 2820 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 〈𝑎, 𝑏〉 → (𝑡 ∈ (𝑐 × 𝑑) ↔ 〈𝑎, 𝑏〉 ∈ (𝑐 × 𝑑))) |
114 | | opelxp 5561 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈𝑎, 𝑏〉 ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑)) |
115 | 113, 114 | bitrdi 290 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 〈𝑎, 𝑏〉 → (𝑡 ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑))) |
116 | 115 | anbi1d 633 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 〈𝑎, 𝑏〉 → ((𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) |
117 | 116 | 2rexbidv 3210 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 〈𝑎, 𝑏〉 → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) ↔ ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) |
118 | 117 | rspccv 3523 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑡 ∈
(◡ − “ 𝑢)∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑡 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) → (〈𝑎, 𝑏〉 ∈ (◡ − “ 𝑢) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) |
119 | 112, 118 | syl5bir 246 |
. . . . . . . . . . . . . . . . . 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 783 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝐺 ∈ TopGrp) |
123 | 57 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑌 ∈ (NrmSGrp‘𝐺)) |
124 | | simprll 779 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑐 ∈ 𝐽) |
125 | 1, 5, 13, 14, 7 | qustgpopn 22871 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑐 ∈ 𝐽) → (𝐹 “ 𝑐) ∈ 𝐾) |
126 | 122, 123,
124, 125 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹 “ 𝑐) ∈ 𝐾) |
127 | | simprlr 780 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑑 ∈ 𝐽) |
128 | 1, 5, 13, 14, 7 | qustgpopn 22871 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑑 ∈ 𝐽) → (𝐹 “ 𝑑) ∈ 𝐾) |
129 | 122, 123,
127, 128 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹 “ 𝑑) ∈ 𝐾) |
130 | 58 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑎 ∈ 𝑋) |
131 | | eceq1 8358 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑎 → [𝑥](𝐺 ~QG 𝑌) = [𝑎](𝐺 ~QG 𝑌)) |
132 | 131, 7, 78 | fvmpt3i 6780 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 ∈ 𝑋 → (𝐹‘𝑎) = [𝑎](𝐺 ~QG 𝑌)) |
133 | 130, 132 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹‘𝑎) = [𝑎](𝐺 ~QG 𝑌)) |
134 | 122, 16 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝐽 ∈ (TopOn‘𝑋)) |
135 | | toponss 21678 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑐 ∈ 𝐽) → 𝑐 ⊆ 𝑋) |
136 | 134, 124,
135 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑐 ⊆ 𝑋) |
137 | | simprrl 781 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑)) |
138 | 137 | simpld 498 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑎 ∈ 𝑐) |
139 | | fnfvima 7006 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 Fn 𝑋 ∧ 𝑐 ⊆ 𝑋 ∧ 𝑎 ∈ 𝑐) → (𝐹‘𝑎) ∈ (𝐹 “ 𝑐)) |
140 | 79, 136, 138, 139 | mp3an2i 1467 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹‘𝑎) ∈ (𝐹 “ 𝑐)) |
141 | 133, 140 | eqeltrrd 2834 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → [𝑎](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑐)) |
142 | 59 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑏 ∈ 𝑋) |
143 | | eceq1 8358 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑏 → [𝑥](𝐺 ~QG 𝑌) = [𝑏](𝐺 ~QG 𝑌)) |
144 | 143, 7, 78 | fvmpt3i 6780 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 ∈ 𝑋 → (𝐹‘𝑏) = [𝑏](𝐺 ~QG 𝑌)) |
145 | 142, 144 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹‘𝑏) = [𝑏](𝐺 ~QG 𝑌)) |
146 | | toponss 21678 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑑 ∈ 𝐽) → 𝑑 ⊆ 𝑋) |
147 | 134, 127,
146 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑑 ⊆ 𝑋) |
148 | 137 | simprd 499 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 𝑏 ∈ 𝑑) |
149 | | fnfvima 7006 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 Fn 𝑋 ∧ 𝑑 ⊆ 𝑋 ∧ 𝑏 ∈ 𝑑) → (𝐹‘𝑏) ∈ (𝐹 “ 𝑑)) |
150 | 79, 147, 148, 149 | mp3an2i 1467 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝐹‘𝑏) ∈ (𝐹 “ 𝑑)) |
151 | 145, 150 | eqeltrrd 2834 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → [𝑏](𝐺 ~QG 𝑌) ∈ (𝐹 “ 𝑑)) |
152 | 141, 151 | opelxpd 5563 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑))) |
153 | 136 | sselda 3877 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ 𝑝 ∈ 𝑐) → 𝑝 ∈ 𝑋) |
154 | 147 | sselda 3877 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ 𝑞 ∈ 𝑑) → 𝑞 ∈ 𝑋) |
155 | 153, 154 | anim12dan 622 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) |
156 | | eceq1 8358 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 𝑝 → [𝑥](𝐺 ~QG 𝑌) = [𝑝](𝐺 ~QG 𝑌)) |
157 | 156, 7, 78 | fvmpt3i 6780 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑝 ∈ 𝑋 → (𝐹‘𝑝) = [𝑝](𝐺 ~QG 𝑌)) |
158 | | eceq1 8358 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 𝑞 → [𝑥](𝐺 ~QG 𝑌) = [𝑞](𝐺 ~QG 𝑌)) |
159 | 158, 7, 78 | fvmpt3i 6780 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑞 ∈ 𝑋 → (𝐹‘𝑞) = [𝑞](𝐺 ~QG 𝑌)) |
160 | | opeq12 4763 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐹‘𝑝) = [𝑝](𝐺 ~QG 𝑌) ∧ (𝐹‘𝑞) = [𝑞](𝐺 ~QG 𝑌)) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 = 〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) |
161 | 157, 159,
160 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 = 〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) |
162 | 155, 161 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 = 〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) |
163 | 123 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → 𝑌 ∈ (NrmSGrp‘𝐺)) |
164 | 1, 5, 24 | quseccl 18454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑝 ∈ 𝑋) → [𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)) |
165 | 1, 5, 24 | quseccl 18454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑞 ∈ 𝑋) → [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻)) |
166 | 164, 165 | anim12dan 622 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻))) |
167 | 163, 155,
166 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ([𝑝](𝐺 ~QG 𝑌) ∈ (Base‘𝐻) ∧ [𝑞](𝐺 ~QG 𝑌) ∈ (Base‘𝐻))) |
168 | | opelxpi 5562 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 18458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → ([𝑝](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) |
171 | 170 | 3expb 1121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ([𝑝](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) |
172 | 163, 155,
171 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ([𝑝](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑞](𝐺 ~QG 𝑌)) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) |
173 | | oveq12 7179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑧 = 𝑝 ∧ 𝑤 = 𝑞) → (𝑧(-g‘𝐺)𝑤) = (𝑝(-g‘𝐺)𝑞)) |
174 | 173 | eceq1d 8359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑧 = 𝑝 ∧ 𝑤 = 𝑞) → [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) |
175 | | ecexg 8324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐺 ~QG 𝑌) ∈ V → [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌) ∈ V) |
176 | 8, 175 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌) ∈ V |
177 | 174, 66, 176 | ovmpoa 7320 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → (𝑝 − 𝑞) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) |
178 | 155, 177 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → (𝑝 − 𝑞) = [(𝑝(-g‘𝐺)𝑞)](𝐺 ~QG 𝑌)) |
179 | 172, 178 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ([𝑝](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑞](𝐺 ~QG 𝑌)) = (𝑝 − 𝑞)) |
180 | | df-ov 7173 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ([𝑝](𝐺 ~QG 𝑌)(-g‘𝐻)[𝑞](𝐺 ~QG 𝑌)) = ((-g‘𝐻)‘〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) |
181 | | df-ov 7173 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑝 − 𝑞) = ( − ‘〈𝑝, 𝑞〉) |
182 | 179, 180,
181 | 3eqtr3g 2796 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ((-g‘𝐻)‘〈[𝑝](𝐺 ~QG 𝑌), [𝑞](𝐺 ~QG 𝑌)〉) = ( − ‘〈𝑝, 𝑞〉)) |
183 | | opelxpi 5562 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑) → 〈𝑝, 𝑞〉 ∈ (𝑐 × 𝑑)) |
184 | | simprrr 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) |
185 | 184 | sselda 3877 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ 〈𝑝, 𝑞〉 ∈ (𝑐 × 𝑑)) → 〈𝑝, 𝑞〉 ∈ (◡ − “ 𝑢)) |
186 | 183, 185 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → 〈𝑝, 𝑞〉 ∈ (◡ − “ 𝑢)) |
187 | | elpreima 6835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ( − Fn
(𝑋 × 𝑋) → (〈𝑝, 𝑞〉 ∈ (◡ − “ 𝑢) ↔ (〈𝑝, 𝑞〉 ∈ (𝑋 × 𝑋) ∧ ( − ‘〈𝑝, 𝑞〉) ∈ 𝑢))) |
188 | 98, 187 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(〈𝑝, 𝑞〉 ∈ (◡ − “ 𝑢) ↔ (〈𝑝, 𝑞〉 ∈ (𝑋 × 𝑋) ∧ ( − ‘〈𝑝, 𝑞〉) ∈ 𝑢)) |
189 | 188 | simprbi 500 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(〈𝑝, 𝑞〉 ∈ (◡ − “ 𝑢) → ( − ‘〈𝑝, 𝑞〉) ∈ 𝑢) |
190 | 186, 189 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → ( − ‘〈𝑝, 𝑞〉) ∈ 𝑢) |
191 | 182, 190 | eqeltrd 2833 |
. . . . . . . . . . . . . . . . . . . . . . . 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 6835 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 2833 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐺 ∈
TopGrp ∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) ∧ (𝑝 ∈ 𝑐 ∧ 𝑞 ∈ 𝑑)) → 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢)) |
198 | 197 | ralrimivva 3103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → ∀𝑝 ∈ 𝑐 ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢)) |
199 | | opeq1 4759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 = (𝐹‘𝑝) → 〈𝑧, 𝑤〉 = 〈(𝐹‘𝑝), 𝑤〉) |
200 | 199 | eleq1d 2817 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 = (𝐹‘𝑝) → (〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ 〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
201 | 200 | ralbidv 3109 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = (𝐹‘𝑝) → (∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
202 | 201 | ralima 7011 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹 Fn 𝑋 ∧ 𝑐 ⊆ 𝑋) → (∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑝 ∈ 𝑐 ∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
203 | 79, 202 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 ⊆ 𝑋 → (∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑝 ∈ 𝑐 ∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
204 | | opeq2 4761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 = (𝐹‘𝑞) → 〈(𝐹‘𝑝), 𝑤〉 = 〈(𝐹‘𝑝), (𝐹‘𝑞)〉) |
205 | 204 | eleq1d 2817 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 = (𝐹‘𝑞) → (〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
206 | 205 | ralima 7011 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹 Fn 𝑋 ∧ 𝑑 ⊆ 𝑋) → (∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
207 | 79, 206 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑑 ⊆ 𝑋 → (∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
208 | 207 | ralbidv 3109 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑑 ⊆ 𝑋 → (∀𝑝 ∈ 𝑐 ∀𝑤 ∈ (𝐹 “ 𝑑)〈(𝐹‘𝑝), 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑝 ∈ 𝑐 ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
209 | 203, 208 | sylan9bb 513 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑐 ⊆ 𝑋 ∧ 𝑑 ⊆ 𝑋) → (∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑝 ∈ 𝑐 ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
210 | 136, 147,
209 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → (∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑝 ∈ 𝑐 ∀𝑞 ∈ 𝑑 〈(𝐹‘𝑝), (𝐹‘𝑞)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
211 | 198, 210 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → ∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢)) |
212 | | dfss3 3865 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑦 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑))𝑦 ∈ (◡(-g‘𝐻) “ 𝑢)) |
213 | | eleq1 2820 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 〈𝑧, 𝑤〉 → (𝑦 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ 〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
214 | 213 | ralxp 5684 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑦 ∈
((𝐹 “ 𝑐) × (𝐹 “ 𝑑))𝑦 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢)) |
215 | 212, 214 | bitri 278 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢) ↔ ∀𝑧 ∈ (𝐹 “ 𝑐)∀𝑤 ∈ (𝐹 “ 𝑑)〈𝑧, 𝑤〉 ∈ (◡(-g‘𝐻) “ 𝑢)) |
216 | 211, 215 | sylibr 237 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢)) |
217 | | xpeq1 5539 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑟 = (𝐹 “ 𝑐) → (𝑟 × 𝑠) = ((𝐹 “ 𝑐) × 𝑠)) |
218 | 217 | eleq2d 2818 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 = (𝐹 “ 𝑐) → (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ↔ 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × 𝑠))) |
219 | 217 | sseq1d 3908 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 = (𝐹 “ 𝑐) → ((𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢) ↔ ((𝐹 “ 𝑐) × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) |
220 | 218, 219 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 = (𝐹 “ 𝑐) → ((〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)) ↔ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × 𝑠) ∧ ((𝐹 “ 𝑐) × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
221 | | xpeq2 5546 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 = (𝐹 “ 𝑑) → ((𝐹 “ 𝑐) × 𝑠) = ((𝐹 “ 𝑐) × (𝐹 “ 𝑑))) |
222 | 221 | eleq2d 2818 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = (𝐹 “ 𝑑) → (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × 𝑠) ↔ 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)))) |
223 | 221 | sseq1d 3908 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = (𝐹 “ 𝑑) → (((𝐹 “ 𝑐) × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢) ↔ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢))) |
224 | 222, 223 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = (𝐹 “ 𝑑) → ((〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × 𝑠) ∧ ((𝐹 “ 𝑐) × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)) ↔ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ∧ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
225 | 220, 224 | rspc2ev 3538 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹 “ 𝑐) ∈ 𝐾 ∧ (𝐹 “ 𝑑) ∈ 𝐾 ∧ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ∧ ((𝐹 “ 𝑐) × (𝐹 “ 𝑑)) ⊆ (◡(-g‘𝐻) “ 𝑢))) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) |
226 | 126, 129,
152, 216, 225 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) ∧ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)))) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) |
227 | 226 | expr 460 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈ TopGrp
∧ 𝑌 ∈
(NrmSGrp‘𝐺)) ∧
𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
228 | 227 | rexlimdvva 3204 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (◡ − “ 𝑢)) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
229 | 121, 228 | syld 47 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ([(𝑎(-g‘𝐺)𝑏)](𝐺 ~QG 𝑌) ∈ 𝑢 → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
230 | 64, 229 | sylbid 243 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) ∈ 𝑢 → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
231 | 230 | adantld 494 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ ((Base‘𝐻) × (Base‘𝐻)) ∧
((-g‘𝐻)‘〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) ∈ 𝑢) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
232 | 55, 231 | sylbid 243 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
233 | | opeq12 4763 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → 〈𝑥, 𝑦〉 = 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉) |
234 | 233 | eleq1d 2817 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) ↔ 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢))) |
235 | 233 | eleq1d 2817 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))} ↔ 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))})) |
236 | | opex 5322 |
. . . . . . . . . . . . . . 15
⊢
〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ V |
237 | | eleq1 2820 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 → (𝑤 ∈ (𝑟 × 𝑠) ↔ 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠))) |
238 | 237 | anbi1d 633 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 → ((𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)) ↔ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
239 | 238 | 2rexbidv 3210 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 → (∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)) ↔ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
240 | 236, 239 | elab 3573 |
. . . . . . . . . . . . . 14
⊢
(〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))} ↔ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) |
241 | 235, 240 | bitrdi 290 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))} ↔ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
242 | 234, 241 | imbi12d 348 |
. . . . . . . . . . . 12
⊢ ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → ((〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → 〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))}) ↔ (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (◡(-g‘𝐻) “ 𝑢) → ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (〈[𝑎](𝐺 ~QG 𝑌), [𝑏](𝐺 ~QG 𝑌)〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))))) |
243 | 232, 242 | syl5ibrcom 250 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → 〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))}))) |
244 | 243 | rexlimdvva 3204 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 (𝑥 = [𝑎](𝐺 ~QG 𝑌) ∧ 𝑦 = [𝑏](𝐺 ~QG 𝑌)) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐻) “ 𝑢) → 〈𝑥, 𝑦〉 ∈ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))}))) |
245 | 50, 244 | sylbird 263 |
. . . . . . . . 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 5632 |
. . . . . 6
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (◡(-g‘𝐻) “ 𝑢) ⊆ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))}) |
249 | | ssabral 3952 |
. . . . . 6
⊢ ((◡(-g‘𝐻) “ 𝑢) ⊆ {𝑤 ∣ ∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))} ↔ ∀𝑤 ∈ (◡(-g‘𝐻) “ 𝑢)∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) |
250 | 248, 249 | sylib 221 |
. . . . 5
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → ∀𝑤 ∈ (◡(-g‘𝐻) “ 𝑢)∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢))) |
251 | | eltx 22319 |
. . . . . . 7
⊢ ((𝐾 ∈
(TopOn‘(Base‘𝐻)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → ((◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ (◡(-g‘𝐻) “ 𝑢)∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
252 | 23, 23, 251 | syl2anc 587 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ((◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ (◡(-g‘𝐻) “ 𝑢)∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
253 | 252 | adantr 484 |
. . . . 5
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → ((◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾) ↔ ∀𝑤 ∈ (◡(-g‘𝐻) “ 𝑢)∃𝑟 ∈ 𝐾 ∃𝑠 ∈ 𝐾 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ (◡(-g‘𝐻) “ 𝑢)))) |
254 | 250, 253 | mpbird 260 |
. . . 4
⊢ (((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) ∧ 𝑢 ∈ 𝐾) → (◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾)) |
255 | 254 | ralrimiva 3096 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → ∀𝑢 ∈ 𝐾 (◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾)) |
256 | | txtopon 22342 |
. . . . 5
⊢ ((𝐾 ∈
(TopOn‘(Base‘𝐻)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → (𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻)))) |
257 | 23, 23, 256 | syl2anc 587 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → (𝐾 ×t 𝐾) ∈ (TopOn‘((Base‘𝐻) × (Base‘𝐻)))) |
258 | | iscn 21986 |
. . . 4
⊢ (((𝐾 ×t 𝐾) ∈
(TopOn‘((Base‘𝐻) × (Base‘𝐻))) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) →
((-g‘𝐻)
∈ ((𝐾
×t 𝐾) Cn
𝐾) ↔
((-g‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) ∧ ∀𝑢 ∈ 𝐾 (◡(-g‘𝐻) “ 𝑢) ∈ (𝐾 ×t 𝐾)))) |
259 | 257, 23, 258 | syl2anc 587 |
. . 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 22842 |
. 2
⊢ (𝐻 ∈ TopGrp ↔ (𝐻 ∈ Grp ∧ 𝐻 ∈ TopSp ∧
(-g‘𝐻)
∈ ((𝐾
×t 𝐾) Cn
𝐾))) |
262 | 3, 26, 260, 261 | syl3anbrc 1344 |
1
⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopGrp) |